Università di Torino
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,
Back to Gian Luca Pozzato's home page