# Questions about SMT logic solvers

• I
• olgerm

#### olgerm

Gold Member
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: