In this paper, we present a preliminary result on the generation of Hilbert proofs for classical propositional logic. This is part of our ongoing research on the comparison of proof-search in different proof-systems. Exploiting the notion of evaluation function, we define a fully deterministic terminating decision procedure that returns either a derivation in the Hilbert calculus of the given goal or a counter model witnessing its unprovability.

Ferrari, M., Fiorentini, C., Fiorino, G. (2019). A Sequent Based On-the-fly Procedure to Get Hilbert Proofs in Classical Propositional Logic. In COMPUTATION TOOLS 2019 The Tenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking.

A Sequent Based On-the-fly Procedure to Get Hilbert Proofs in Classical Propositional Logic

Fiorino, G
2019

Abstract

In this paper, we present a preliminary result on the generation of Hilbert proofs for classical propositional logic. This is part of our ongoing research on the comparison of proof-search in different proof-systems. Exploiting the notion of evaluation function, we define a fully deterministic terminating decision procedure that returns either a derivation in the Hilbert calculus of the given goal or a counter model witnessing its unprovability.
slide + paper
Automated Theorem Proving; Hilbert calculi.
English
COMPUTATION TOOLS 2019 The Tenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking
2019
Rückemann, CP
COMPUTATION TOOLS 2019 The Tenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking
978-1-61208-709-2
2019
open
Ferrari, M., Fiorentini, C., Fiorino, G. (2019). A Sequent Based On-the-fly Procedure to Get Hilbert Proofs in Classical Propositional Logic. In COMPUTATION TOOLS 2019 The Tenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking.
File in questo prodotto:
File Dimensione Formato  
hilbertProcedureEval.pdf

accesso aperto

Descrizione: Versione dell'articolo sottomessa alla conferenza
Tipologia di allegato: Submitted Version (Pre-print)
Dimensione 207.52 kB
Formato Adobe PDF
207.52 kB 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/10281/258998
Citazioni
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
Social impact