We present hypersequent calculi for the strongest logics in Lewis' family of conditional systems, characterized by uniformity and total reflexivity. We first present a non-standard hypersequent calculus, which allows a syntactic proof of cut elimination. We then introduce standard hypersequent calculi, in which sequents are enriched by additional structures to encode plausibility formulas and diamond formulas. Proof search using these calculi is terminating, and the completeness proof shows how a countermodel can be constructed from a branch of a failed proof search. We then describe tuCLEVER, a theorem prover that implements the standard hypersequent calculi. The prover provides a decision procedure for the logics, and it produces a countermodel in case of proof search failure. The prover tuCLEVER is inspired by the methodology of leanTAP and it is implemented in Prolog. Preliminary experimental results show that the performances of tuCLEVER are promising.

Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning

Pozzato G. L.
2022-01-01

Abstract

We present hypersequent calculi for the strongest logics in Lewis' family of conditional systems, characterized by uniformity and total reflexivity. We first present a non-standard hypersequent calculus, which allows a syntactic proof of cut elimination. We then introduce standard hypersequent calculi, in which sequents are enriched by additional structures to encode plausibility formulas and diamond formulas. Proof search using these calculi is terminating, and the completeness proof shows how a countermodel can be constructed from a branch of a failed proof search. We then describe tuCLEVER, a theorem prover that implements the standard hypersequent calculi. The prover provides a decision procedure for the logics, and it produces a countermodel in case of proof search failure. The prover tuCLEVER is inspired by the methodology of leanTAP and it is implemented in Prolog. Preliminary experimental results show that the performances of tuCLEVER are promising.
2022
32
2
233
280
Girlando M.; Lellmann B.; Olivetti N.; Pesce S.; Pozzato G.L.
File in questo prodotto:
File Dimensione Formato  
JLC_GirLelOliPozPes-SUBMITTED - NEW.pdf

Accesso riservato

Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 2.31 MB
Formato Adobe PDF
2.31 MB 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: https://hdl.handle.net/2318/1853618
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact