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

First Order Stålmarck

Magnus Björk (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Journal of Automated Reasoning (0168-7433). Vol. 42 (2009), 1, p. 99-122.
[Artikel, refereegranskad vetenskaplig]

We present a proof method with a novel way of introducing universal lemmas. The method is a first order extension of StAyenlmarck's method, containing a branch-and-merge rule known as the dilemma rule. The dilemma rule creates two branches in a tableau-like way, but later recombines the two branches, keeping the common consequences. While the propositional version uses normal set intersection in the merges, the first order version searches for pairwise unifiable formulae in the two branches. Within branches, the system uses a special kind of variables that may not be substituted. At branch merges, these variables are replaced by universal variables, and in this way universal lemmas can be introduced. Relevant splitting formulae are found through failed unifications of variables in branches. This article presents the calculus and proof procedure, and shows soundness and completeness. Benchmarks of an implementation are also presented.

Nyckelord: Automated theorem proving, First order logic, Stalmarck's method, Universal lemmas, Intersections, model evolution calculus, quantification theory, logic



Denna post skapades 2010-02-23.
CPL Pubid: 114219

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur