### Skapa referens, olika format (klipp och klistra)

**Harvard**

Björk, M. (2003) *Stålmarck's Method for Automated Theorem Proving in First Order Logic*. Göteborg : Chalmers University of Technology (Technical report L - School of Computer Science and Engineering, Chalmers University of Technology, nr: 28).

** BibTeX **

@book{

Björk2003,

author={Björk, Magnus},

title={Stålmarck's Method for Automated Theorem Proving in First Order Logic},

abstract={We present an extension of Stålmarck's method to classical first order predicate logic. Stålmarck's method is a satisfiability checking method for propositional logic, and it resembles tableaux and KE. Its most distinctive feature is the dilemma rule, which is an extended branching rule, that allows branches to be recombined. This is done by keeping the intersection of all derived consequences in the two branches after the merge. Stålmarck's method for propositional logic is known to be sound and complete, and has turned out to be efficient in industrial applications.
The extension of Stålmarck's method uses a tableaux-like calculus with both universal and rigid variables. We define a notion of logical intersections, in which the pairwise unifiable formulas from two sets of formulas are found. We also describe how rigid variables can be transformed into universal variables, when the two branches of a dilemma rule are merged. We define the proof system rigorously, and prove that it is sound. We also prove the specialized derivations theorem, which states that instantiating a rigid variable in all steps of a proof preserves proof correctness. We then outline a proof procedure, and discuss some of its features. A prototype implementing parts of the proof procedure has been made.},

publisher={Institutionen för datavetenskap, Formella metoder, Chalmers tekniska högskola,},

place={Göteborg},

year={2003},

series={Technical report L - School of Computer Science and Engineering, Chalmers University of Technology, no: 28},

keywords={Stålmarck's method, automated theorem proving, first order logic, tableaux},

note={94},

}

** RefWorks **

RT Dissertation/Thesis

SR Print

ID 1980

A1 Björk, Magnus

T1 Stålmarck's Method for Automated Theorem Proving in First Order Logic

YR 2003

AB We present an extension of Stålmarck's method to classical first order predicate logic. Stålmarck's method is a satisfiability checking method for propositional logic, and it resembles tableaux and KE. Its most distinctive feature is the dilemma rule, which is an extended branching rule, that allows branches to be recombined. This is done by keeping the intersection of all derived consequences in the two branches after the merge. Stålmarck's method for propositional logic is known to be sound and complete, and has turned out to be efficient in industrial applications.
The extension of Stålmarck's method uses a tableaux-like calculus with both universal and rigid variables. We define a notion of logical intersections, in which the pairwise unifiable formulas from two sets of formulas are found. We also describe how rigid variables can be transformed into universal variables, when the two branches of a dilemma rule are merged. We define the proof system rigorously, and prove that it is sound. We also prove the specialized derivations theorem, which states that instantiating a rigid variable in all steps of a proof preserves proof correctness. We then outline a proof procedure, and discuss some of its features. A prototype implementing parts of the proof procedure has been made.

PB Institutionen för datavetenskap, Formella metoder, Chalmers tekniska högskola,

T3 Technical report L - School of Computer Science and Engineering, Chalmers University of Technology, no: 28

LA eng

OL 30