z3first-order-logicsatisfiabilitysat-solvers

Tool/Language to check Satisfiability of First order logic?

In general, First Order logic is Undecidable. However, Some fragments of first-order logic as Monadic logics, BSR Fragments, Separated Fragments are decidable.

There exist tools to solve SAT/SMT Solvers as Z3. Is there any tool/Language which checks the satisfiability of FOL formulas?

Solution

  • SMT solvers, like Z3, can attempt to check satisfiability of FOL (even 2nd order logic!), though performance might not be great (depending on how the problem looks like) There are also dedicated FOL provers (aka TPTP solvers), like Vampire, E, iProver, etc. See more here: https://en.wikipedia.org/wiki/Automated_theorem_proving