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

**Harvard**

Björk, M. (2006) *A First Order Extension of Stålmarck's Method*. Göteborg : Chalmers University of Technology (Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, nr: 2451).

** BibTeX **

@book{

Björk2006,

author={Björk, Magnus},

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

isbn={91-7291-769-5},

abstract={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. If neither of the branches turns out to be contradictory, then the branches are merged into one branch again, retaining the common consequences of the two branches.
We present a first order version of Stålmarck's method. When branches are merged in first order logic, variables occurring in the respective branches are unified, to retain as much information as possible. We show that variables introduced in dilemma formulae must be treated rigidly in the branches of the dilemma where they were introduced, but that they are universal during and after the merge. Thus, the dilemma rule can be used to introduce lemmas with universal variables.
We also present a proof procedure that searches for shallow dilemma proofs. It begins by searching for proofs not including the dilemma rule, then extends the search with non-nested dilemmas. After that, proofs with at most two simultaneously open dilemmas are found, then with three, and so on. The proof procedure does not substitute rigid variables destructively; instead it explores an instance of the current dilemma, after the branches have been merged. This is done to preserve as many generalized conclusions as possible, and to be able to find new dilemma formulae.
We show that the calculus and proof procedure are sound and complete. We present encouraging benchmarks for the automated theorem prover Dilemma, that is based on the method. },

publisher={Institutionen för data- och informationsteknik, Datavetenskap (Chalmers), Chalmers tekniska högskola,},

place={Göteborg},

year={2006},

series={Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, no: 2451Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, no: 15D},

keywords={ Automated Theorem Proving, Tableaux, Stålmarck's Method},

note={133},

}

** RefWorks **

RT Dissertation/Thesis

SR Print

ID 19666

A1 Björk, Magnus

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

YR 2006

SN 91-7291-769-5

AB 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. If neither of the branches turns out to be contradictory, then the branches are merged into one branch again, retaining the common consequences of the two branches.
We present a first order version of Stålmarck's method. When branches are merged in first order logic, variables occurring in the respective branches are unified, to retain as much information as possible. We show that variables introduced in dilemma formulae must be treated rigidly in the branches of the dilemma where they were introduced, but that they are universal during and after the merge. Thus, the dilemma rule can be used to introduce lemmas with universal variables.
We also present a proof procedure that searches for shallow dilemma proofs. It begins by searching for proofs not including the dilemma rule, then extends the search with non-nested dilemmas. After that, proofs with at most two simultaneously open dilemmas are found, then with three, and so on. The proof procedure does not substitute rigid variables destructively; instead it explores an instance of the current dilemma, after the branches have been merged. This is done to preserve as many generalized conclusions as possible, and to be able to find new dilemma formulae.
We show that the calculus and proof procedure are sound and complete. We present encouraging benchmarks for the automated theorem prover Dilemma, that is based on the method.

PB Institutionen för data- och informationsteknik, Datavetenskap (Chalmers), Chalmers tekniska högskola,

T3 Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, no: 2451Technical report D - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, no: 15D

LA eng

OL 30