In this work we introduce a labelled sequent calculus for Conditional Logics admitting the axiom of Conditional Excluded Middle (CEM), rejected by Lewis but endorsed by Stalnaker. We also consider some of its standard extensions. Conditional Logics with CEM recently have received a renewed attention and have found several applications in knowledge representation and artificial intelligence. The proposed calculus improves the only existing one, SeqS, where the condition CEM on conditional models is tackled by means of a simple but computationally expensive process of label substitution. Here we propose an alternative calculus avoiding label substitution, where a single rule deals simultaneously with conditional formulas and the CEM axiom. We have implemented the calculi in Prolog following the “lean” methodology, then we have tested the performances of the prover and compared them with those of CondLean, an implementation of SeqS. The performances are promising and better than those of CondLean, witnessing that the proposed calculus provides an effective improvement with respect to the state of the art.

Efficient Theorem Proving for Conditional Logics with Conditional Excluded Middle

Pozzato G. L.
2022-01-01

Abstract

In this work we introduce a labelled sequent calculus for Conditional Logics admitting the axiom of Conditional Excluded Middle (CEM), rejected by Lewis but endorsed by Stalnaker. We also consider some of its standard extensions. Conditional Logics with CEM recently have received a renewed attention and have found several applications in knowledge representation and artificial intelligence. The proposed calculus improves the only existing one, SeqS, where the condition CEM on conditional models is tackled by means of a simple but computationally expensive process of label substitution. Here we propose an alternative calculus avoiding label substitution, where a single rule deals simultaneously with conditional formulas and the CEM axiom. We have implemented the calculi in Prolog following the “lean” methodology, then we have tested the performances of the prover and compared them with those of CondLean, an implementation of SeqS. The performances are promising and better than those of CondLean, witnessing that the proposed calculus provides an effective improvement with respect to the state of the art.
2022
37th Italian Conference on Computational Logic, CILC 2022
Bologna
2022
CEUR Workshop Proceedings
CEUR-WS
3204
217
231
conditional logics; proof methods; sequent calculi; theorem proving
Panic N.; Pozzato G.L.
File in questo prodotto:
File Dimensione Formato  
paper_22.pdf

Accesso aperto

Dimensione 1.49 MB
Formato Adobe PDF
1.49 MB Adobe PDF Visualizza/Apri

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: https://hdl.handle.net/2318/1890095
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact