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

Extending Stålmarck's Method to First Order Logic

Magnus Björk (Institutionen för datavetenskap, Formella metoder)
TABLEAUX 2003 Position Papers and Tutorials (2003)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Stålmarck's method, first order logic, automated theorem proving

Denna post skapades 2006-09-28. Senast ändrad 2013-08-12.
CPL Pubid: 2265


Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)


Information Technology

Chalmers infrastruktur