Sökning: "Theorem Proving"

Visar resultat 21 - 25 av 43 avhandlingar innehållade orden Theorem Proving.

  1. 21. 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

  3. 22. A First Order Extension of Stålmarck's Method

    Författare :Magnus Björk; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Tableaux; Automated Theorem Proving; Stålmarck s Method;

    Sammanfattning : Stålmarck's method is an algorithm that decides validity of formulae in propositional logic. It resembles many tableaux method, but uses a special branch-and-merge-rule, called the dilemma rule. The dilemma rule creates two branches, where a formula (called the dilemma formula) is assumed to be false in one branch and true in the other one. LÄS MER

  4. 23. Essays on Mathematical Economics

    Författare :Uuganbaatar Ninjbat; Handelshögskolan i Stockholm; []
    Nyckelord :SAMHÄLLSVETENSKAP; SOCIAL SCIENCES;

    Sammanfattning : .... LÄS MER

  5. 24. On Simultaneous Rigid E-Unification

    Författare :Margus Veanes; Andrei Voronkov; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Datalogi; Computing Science;

    Sammanfattning : Automated theorem proving methods in classical logic with equality that are based on the Herbrand theorem, reduce to a problem called Simultaneous Rigid E-Unification, or SREU for short. Recent developments show that SREU has also close connections with intuitionistic logic with equality, second-order unification, some combinatorial problems and finite tree automata. LÄS MER

  7. 25. Towards a practical programming language based on dependent type theory

    Författare :Ulf Norell; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; dependent types; type theory; metavariables; programming; pattern matching; type checking;

    Sammanfattning : Dependent type theories have a long history of being used for theorem proving. One aspect of type theory which makes it very powerful as a proof language is that it mixes deduction with computation. LÄS MER