CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Magnus Björk (Institutionen för datavetenskap, Formella metoder)
Göteborg : Chalmers University of Technology, 2003. - 94 s.

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.

Nyckelord: Stålmarck's method, automated theorem proving, first order logic, tableaux

Denna post skapades 2006-09-28. Senast ändrad 2013-08-12.
CPL Pubid: 1980


Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)


Information Technology

Chalmers infrastruktur


Datum: 2003-11-13

Ingår i serie

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