Search for dissertations about: "Theorem Proving"

Showing result 1 - 5 of 28 swedish dissertations containing the words Theorem Proving.

  1. 1. Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving

    Author : Hans Svensson; [2008]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; distributed algorithms; fault-tolerance; theorem proving; verification; distributed programming; Erlang; model checking; testing;

    Abstract : Software infiltrates every aspect of modern society. Production, transportation, entertainment, and almost every other sphere that influences modern living are either directly or indirectly dependent on software systems. READ MORE

  2. 2. Automated Theorem Proving with Extensions of First-Order Logic

    University dissertation from ; Chalmers tekniska högskola; Gothenburg

    Author : Evgenii Kotelnikov; [2018]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; clausal normal form; Program Verification; automated theorem proving; program analysis; TPTP; Vampire; first-order logic;

    Abstract : Automated theorem provers are computer programs that check whether a logical conjecture follows from a set of logical statements. The conjecture and the statements are expressed in the language of some formal logic, such as first-order logic. READ MORE

  3. 3. Theory Exploration and Inductive Theorem Proving

    University dissertation from ; Chalmers tekniska högskola; Gothenburg

    Author : Dan Rosén; [2016]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES;

    Abstract : We have built two state-of-the-art inductive theorem provers named HipSpec and Hipster. The main issue when automating proofs by induction is to discover essential helper lemmas. Our theorem provers use the technique theory exploration, which is a method to systematically discover interesting conclusions about a mathematical theory. READ MORE

  4. 4. Proving and Disproving in Dynamic Logic for Java

    University dissertation from Göteborg : Chalmers University of Technology

    Author : Philipp Rümmer; Göteborgs universitet.; Gothenburg University.; [2006]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; theorem proving; disproving; dynamic logic; program verification; testing;

    Abstract : This thesis is about proving the functional correctness and incorrectness of imperative, object-oriented programs. One of the main approaches for the first item is deductive program verification, whereas the second item is traditionally handled by techniques like testing. READ MORE

  5. 5. Automated Theorem Proving in a First-Order Logic with First class Boolean Sort

    University dissertation from Göteborg : Chalmers University of Technology

    Author : Evgenii Kotelnikov; [2016]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; first-order logic; program analysis; program verification; TPTP; automated theorem proving; Vampire;

    Abstract : Automated theorem proving is one of the central areas of computer mathematics. It studies methods and techniques for establishing validity of mathematical problems using a computer. The problems are expressed in a variety of formal logics, including first-order logic. READ MORE