We present proof methods for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We introduce tableaux calculi (called TST) for all KLM logics. We provide decision procedures for KLM logics based on these calculi, and we study their complexity. Finally, we describe KLMLean 2.0, a theorem prover implementing the calculi TST inspired by the “lean” methodology. KLMLean 2.0 is implemented in SICStus Prolog and it also comprises a graphical interface written in Java.
KLM Logics of Nonmonotonic Reasoning: Calculi and Implementations
GLIOZZI, Valentina;POZZATO, GIAN LUCA
2007-01-01
Abstract
We present proof methods for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We introduce tableaux calculi (called TST) for all KLM logics. We provide decision procedures for KLM logics based on these calculi, and we study their complexity. Finally, we describe KLMLean 2.0, a theorem prover implementing the calculi TST inspired by the “lean” methodology. KLMLean 2.0 is implemented in SICStus Prolog and it also comprises a graphical interface written in Java.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
