We describe an extension of Stålmarck's method in First Order Logic. Stålmarck's method is a tableaux-like theorem proving method for propositional logic, that uses a branch-and-merge rule known as the dilemma rule. This rule opens two branches and later merges them, by retaining their common consequences. The propositional version does this with normal set intersection, while the FOL version searches for pairwise unifiable formulae from the two branches. The proof procedure attempts to find proofs with as few simultaneously open branches as possible. We present the proof system and a proof procedure, and show soundness and completeness. We also present benchmarks for an implementation of the proof procedure. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Björk, M. (2005). A first order extension of stålmarck’s method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3835 LNAI, pp. 276–291). Springer Verlag. https://doi.org/10.1007/11591191_20
Mendeley helps you to discover research relevant for your work.