Is there a prover just for propositional logic

Question

I tried to implement LTL logic syntactically using the axiomatization command, with the purpose of automatically finding proofs for theorems (motivation of proving program properties).

However the automatic provers such as (cvc4, z3, e, etc) all use quantifiers of some sort. For example using FOL one could prove F(p)-->G(p) which is obviously false.

My question is if there exists a prover, just like the ones mentioned, but that is made for propositional logic, i.e. only has access to MP and the propositional logic axioms.

I am rather new to isabelle so there might be an easier way of doing this im not seeing.

EDIT: I am looking for a hilbert style deduction prover and not a SAT as this would defeat the problem of implementing it axiomatically

Answer 1

I think the sat method only uses propositional logic.

However, I would recommend not to use axiomatizations and just define the syntax of LTL using datatypes and the semantics using functions. Maybe you can reuse the formalization from https://www.isa-afp.org/entries/LTL.html

Without axiomatizations you are then free to use any method.

Answer 2

What you want is a SAT solver, such as minisat.

However the automatic provers such as (cvc4, z3, e, etc) all use quantifiers of some sort. For example using FOL one could prove F(p)-->G(p) which is obviously false.

This is not correct. Any first-order theorem prover, like iProver, E, Vampire, will not prove forall X. f(X) => g(x).