Home // COMPUTATION TOOLS 2019, The Tenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

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

Authors:
Mauro Ferrari
Camillo Fiorentini
Guido Fiorino

Keywords: Automated Theorem Proving; Hilbert calculi.

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.

Pages: 10 to 15

Copyright: Copyright (c) IARIA, 2019

Publication date: May 5, 2019

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-709-2

Location: Venice, Italy

Dates: from May 5, 2019 to May 9, 2019