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

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.