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.
Citazione: | 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. | |
Tipo: | slide + paper | |
Carattere della pubblicazione: | Scientifica | |
Presenza di un coautore afferente ad Istituzioni straniere: | No | |
Titolo: | A Sequent Based On-the-fly Procedure to Get Hilbert Proofs in Classical Propositional Logic | |
Autori: | Ferrari, M; Fiorentini, C; Fiorino, G | |
Autori: | FIORINO, GUIDO GIUSEPPE (Corresponding) | |
Data di pubblicazione: | 2019 | |
Lingua: | English | |
Nome del convegno: | COMPUTATION TOOLS 2019 The Tenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking | |
ISBN: | 978-1-61208-709-2 | |
Appare nelle tipologie: | 02 - Intervento a convegno |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
hilbertProcedureEval.pdf | Versione dell'articolo sottomessa alla conferenza | Preprint | Open Access Visualizza/Apri |