We present FreeP 1.0, a theorem prover for the KLM preferential logic P of nonmonotonic reasoning. FreeP 1.0 is a SICStus Prolog implementation of a free-variables, labelled tableau calculus for P, obtained by introducing suitable modalities to interpret conditional assertions. The performances of FreeP 1.0 are promising. FreeP 1.0 can be downloaded at http:// www.di.unito.it/ ∼pozzato/FreeP 1.0.

An Implmentation of a Free-variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: the Theorem Prover FreeP 1.0

GLIOZZI, Valentina;POZZATO, GIAN LUCA
2007

Abstract

We present FreeP 1.0, a theorem prover for the KLM preferential logic P of nonmonotonic reasoning. FreeP 1.0 is a SICStus Prolog implementation of a free-variables, labelled tableau calculus for P, obtained by introducing suitable modalities to interpret conditional assertions. The performances of FreeP 1.0 are promising. FreeP 1.0 can be downloaded at http:// www.di.unito.it/ ∼pozzato/FreeP 1.0.
AI*IA 2007 (10th Congress of Italian Association for Artificial Intelligence)
Roma, Italia
September 2007
4733
84
96
http://link.springer.com/chapter/10.1007/978-3-540-74782-6_9?LI=true
Tableaux Calculi; Nonomonotonic Reasoning; Theorem Proving
L. GIORDANO; V. GLIOZZI; N. OLIVETTI; G. POZZATO
File in questo prodotto:
File Dimensione Formato  
AI*IA 2007.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 568.64 kB
Formato Adobe PDF
568.64 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2318/28984
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact