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 a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema): $$\begin{align} & (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\ & (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\ & (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\ & (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\ & (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\ & (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber...

Similar threads

Back
Top