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

**Harvard**

Björk, M. (2005) *A First Order Extension of Stålmarck's Method*.

** BibTeX **

@conference{

Björk2005,

author={Björk, Magnus},

title={A First Order Extension of Stålmarck's Method},

booktitle={Logic for Programming, Artificial Intelligence, and Reasoning, 2005, Montego Bay, Jamaica},

isbn={978-3-540-30553-8},

pages={276-291},

abstract={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.},

year={2005},

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

}

** RefWorks **

RT Conference Proceedings

SR Print

ID 9839

A1 Björk, Magnus

T1 A First Order Extension of Stålmarck's Method

YR 2005

T2 Logic for Programming, Artificial Intelligence, and Reasoning, 2005, Montego Bay, Jamaica

SN 978-3-540-30553-8

SP 276

OP 291

AB 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.

LA eng

OL 30