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

Appendix to Extending Stålmarck's Method to First Order Logic

Magnus Björk (Institutionen för datavetenskap, Formella metoder)
Göteborg : Chalmers University of Technology, 2003. - 26 s.
[Rapport]

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



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

 

Institutioner (Chalmers)

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

Ämnesområden

Information Technology

Chalmers infrastruktur

Ingår i serie

Technical report - Department of Computing Science, Chalmers University of Technology and Göteborg University 2003-08