Sökning: "sequent calculus"

Hittade 5 avhandlingar innehållade orden sequent calculus.

  1. 1. A Natural Interpretation of Classical Proofs

    Författare :Jens Brage; Per Martin-Löf; Sara Negri; Stockholms universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Brouwer-Heyting-Kolmogorov; classical logic; constructive type theory; constructive semantics; proof interpretation; double-negation; continuation-passing-style; natural deduction; sequent calculus; cut elimination; explicit substitution; Mathematical logic; Matematisk logik;

    Sammanfattning : In this thesis we use the syntactic-semantic method of constructive type theory to give meaning to classical logic, in particular Gentzen's LK.We interpret a derivation of a classical sequent as a derivation of a contradiction from the assumptions that the antecedent formulas are true and that the succedent formulas are false, where the concepts of truth and falsity are taken to conform to the corresponding constructive concepts, using function types to encode falsity. LÄS MER

  3. 2. Towards a Deductive Compilation Approach

    Författare :Ran Ji; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Software Engineering; Software Verification; Partial Evaluation; Symbolic Execution; Deductive Compilation;

    Sammanfattning : Software correctness is an important topic, however, it is difficult to achieve. This thesis is a step towards a new way to ensure the software correctness in both source code and bytecode level. KeY is a state-of-the-art verification tool for Java source code. LÄS MER

  4. 3. New techniques for handling quantifiers in Boolean and first-order logic

    Författare :Peter Backeman; Philipp Rümmer; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Datavetenskap med inriktning mot inbyggda system; Computer Science with specialization in Embedded Systems;

    Sammanfattning : The automation of reasoning has been an aim of research for a long time. Already in 17th century, the famous mathematician Leibniz invented a mechanical calculator capable of performing all four basic arithmetic operators. LÄS MER

  5. 4. Quantifiers and Theories : A Lazy Approach

    Författare :Peter Backeman; Philipp Rümmer; Jie-Hong Roland Jiang; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Automated Reasoning; Automated Theorem Proving; SMT; Unification; Datavetenskap med inriktning mot inbyggda system; Computer Science with specialization in Embedded Systems;

    Sammanfattning : In this thesis we study Automated Theorem Proving (ATP) as well as Satisfiability Modulo Theories (SMT) and present lazy strategies for improving reasoning within these areas. A lazy strategy works by simplifying a problem, and gradually refines the abstraction only when necessary. LÄS MER

  7. 5. GCLA : the design, use and implementation of a program development system

    Författare :Martin Aronsson; Stockholms universitet; []
    Nyckelord :;

    Sammanfattning : We present a program development system, GCLA (Generalized horn Clause LAnguage*), which is based on a generalization of Horn clauses (e.g. Prolog). This generalization takes a quite different view of the meaning of a logic program - a "definitional" view rather than the traditional logical view. LÄS MER