Università di Torino

Laura Giordano, Valentina Gliozzi, Andrea Laspisa, Nicola Olivetti, and Gian Luca Pozzato

KLMOptimal: a theorem prover for KLM Preferential Logic P of Non-monotonic reasoning

Kraus, Lehmann and Magidor (KLM) proposed a formalization of non-monotonic reasoning that was early recognized as a landmark. KLMOptimal is a theorem prover implementing an optimal decision procedure for preferential logic P. It is written in SICStus Prolog and it is inspired by the lean methodology. In this page you will find all you need to run and use KLMOptimal. If you need some help, please contact: pozzato[at]di.unito.it

  SICStus Prolog source code

   Back to Gian Luca Pozzato's home page