Extending Stålmarck's Method to First Order Logic
Magnus Björk · Chalmers Publication Library (Chalmers University of Technology) · 2003
Stålmarck's method is a proof method which resembles tableaux, but which, instead of branching, has a special branch and merge rule, called the dilemma rule. The propositional version was presented several years ago, and we are now working on a version in first order logic. There is an implementation that shows encouraging results. We will briefly describe the proof system and the proof procedure and show the interesting parts of the soundness proof.