First Order Stålmarck

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

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Nyckelord

Universal lemmas

quantification theory

model evolution calculus

First order logic

Stalmarck's method

Automated theorem proving

logic

Intersections

Publikations- och innehållstyp

art (ämneskategori)

ref (ämneskategori)