I Questions about SMT logic solvers

  • I
  • Thread starter Thread starter olgerm
  • Start date Start date
  • Tags Tags
    Logic
AI Thread Summary
SMT solvers like Z3 cannot always check the consistency of first-order logic formulas due to the undecidability of first-order logic, which implies that no algorithm can universally determine consistency for all such formulas. Similarly, Gödel's second incompleteness theorem suggests that no algorithm can check the consistency of all second-order logic formulas. While there are algorithms for specific cases, no general solution exists for second-order logic. Users are encouraged to explore existing resources or contact Z3 developers for insights into unsolvable problems. The discussion highlights the limitations of current SMT solvers in addressing complex logical consistency issues.
olgerm
Gold Member
Messages
532
Reaction score
35
Are smt-solvers (like z3) theoretically able to (always correctly) check consistency of any 1.-order logic formula?
Does it follow from The undecidability of first order logic, that an algorithm, that could check consistency of any 1.-order logic formula, does not exist?
How does the algorithm of work in details? (link to explanation)
Are there any algorithms that could check consistency of any 2.-order logic formula?
Does Gödels 2. incompleteness theorem claim, that such algortihm, that could check consistency of any 2.-order logic formula, does not exist.
Are there any computerprograms that could check consistency of any 2.-order logic formula?

To explain what I mean by 1.-order logic formula I will write here a few examples:
  • ##\exists_{x_1}(A(x_1))\land \neg \exists_{x_1}(A(x_1))##
  • ##\exists_{x_1}(\exists_{x_2}(A(x_1,x_2)\land \exists_{x_3}(A(x_2,x_3)\land A(x_2,x_2))))\land \neg \exists_{x_1}(\exists_{x_2}(\exists_{x_3}( A(x_2,x_1)\land A(x_1,x_3)\land A(x_1,x_1))))##
  • ##\exists_{x_1}(m(x_1) \land \neg\exists_{x_2}(M(x_1, x_2) \land \exists_{x_3}(M(x_1, x_3) \land \neg M(x_2, x_3) \land M(x_3, x_1)) \land \exists_{x_3}(M(x_1, x_3) \land M(x_2, x_3)) \land \neg \exists_{x_3}(M(x_2, x_3) \land M(x_3, x_3))))\land \exists_{x_1}(\exists_{x_2}(m(x_2)\land M(x_2,x_1)\land \exists_{x_3}(M(x_1,x_3)\land M(x_2,x_3))\land \exists_{x_3}(M(x_2,x_3)\land M(x_3,x_2)\land \neg M(x_1,x_3)))\land \neg \exists(M(x_2,x_1)\land M(x_2,x_2)))\lor\exists_{x_1}(M(x_1,x_1)\land \neg \exists_{x_2}(M(x_1,x_2)\land M(x_2,x_2)\land M(x_2,x_1)))##
 
Last edited:
Physics news on Phys.org
I have an idea for smt-solver algorithm myself. Some details are still unclear. It is quite long. I can not post it here very well. Were do you think I could find someone who were interested of it? Should I contact makers of z3?
 
Which mathematical problems z3 can not solve? (I am asking a few examples of simpler mathematical problems/tasks, that z3 can not solve)?
 
I was reading documentation about the soundness and completeness of logic formal systems. Consider the following $$\vdash_S \phi$$ where ##S## is the proof-system making part the formal system and ##\phi## is a wff (well formed formula) of the formal language. Note the blank on left of the turnstile symbol ##\vdash_S##, as far as I can tell it actually represents the empty set. So what does it mean ? I guess it actually means ##\phi## is a theorem of the formal system, i.e. there is a...

Similar threads

Back
Top