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