The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a formula in the modal logic K. To this aim, we design a forward calculus to check the K-satisfiability of a set of modal formulas. From a derivation of Ξ, we can extract a Kripke model of Ξ.

Forward countermodel construction in modal Logic K / M. Ferrari, C. Fiorentini, G. Fiorino (CEUR WORKSHOP PROCEEDINGS). - In: CILC 2018 : Italian Conference on Computational Logic / [a cura di] P. Felli, M. Montali. - [s.l] : CEUR-WS, 2018. - pp. 75-81 (( Intervento presentato al 33. convegno Italian Conference on Computational Logic tenutosi a Bolzano nel 2018.

Forward countermodel construction in modal Logic K

C. Fiorentini;
2018

Abstract

The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a formula in the modal logic K. To this aim, we design a forward calculus to check the K-satisfiability of a set of modal formulas. From a derivation of Ξ, we can extract a Kripke model of Ξ.
Computer Science (all)
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
http://ceur-ws.org/Vol-2214/paper8.pdf
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
2018_cilc.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 543.2 kB
Formato Adobe PDF
543.2 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

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/2434/595703
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact