1
$\begingroup$

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. I realize that some quantified predicate formulas with an arity above 2 are undecidable. But I'm not sure if all of them are provably undecidable. If they are not provably undecidable, then is there an SMT algorithm that can solve quantified n-ary predicate formulas even if sometimes the procedure will not terminate?

Note that for my use case, I'm restricting the model to a finite domain if that helps at all. Yes I'm aware of Trakhtenbrot's theorem.

Sources:

  1. Kroening, D., & Strichman, O. (2016). Decision procedures an algorithmic point of view. Springer.
Improve this question
$\endgroup$
3
  • $\begingroup$ What do you mean by "all of them are provably undecidable"? Presumably there are some trivial cases that are solvable -- undecidability is about worst-case hardness, not a claim that all instances are hard. What am I missing? $\endgroup$
    – D.W. ♦
    Jan 7 at 20:40
  • $\begingroup$ @D.W. I'm saying that undesirability is used as a reason to use fragments of FOL instead. "all of them" refers to SAT for all formulas accepted by FOL. $\endgroup$
    – Vivek Joshy
    Jan 7 at 22:06
  • $\begingroup$ Since the bot bumped this question, it might be better asked in Proof Assistants. $\endgroup$
    – Pseudonym ♦
    Jun 7 at 2:37

1 Answer 1

Reset to default
0
$\begingroup$

You ask two questions. I start by answering your first question.

Undecidability is a worst-case property, which says there is no single algorithm that can work for all problem instances. But some problem instances are, intuitively, "easier". There are problem instances that can be solved. For instance, if you only have a single instance you want to solve, you can write down an algorithm that correctly solves that one instance (it hardcodes the correct answer to that one instance in its source code).

So, in general, it makes no sense to talk about the hardness of a single problem instance -- at least, this is not something we can formalize with the mathematical machinery of undecidability. Rather, we have to talk about the hardness (decidability) of entire classes of problem instances.

Yes, there is an algorithm that can sometimes solve such instances. For instance, you could create an algorithm that hardcodes the correct answer to one instance (input) in its source code, and loops forever on all other inputs. This is correct from a theoretical perspective, but unlikely to be useful in practice.

So, I suspect you are asking from a more pragmatic perspective: I suspect you are hoping for an algorithm that is often successful on many inputs, but is not guaranteed to terminate. Unfortunately I don't know the answer to that. Sorry.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I was hoping and assuming there was something like DPLL(T) that resolves n-ary predicates. $\endgroup$
    – Vivek Joshy
    Jan 7 at 22:30
  • $\begingroup$ @daegontaven, OK. Sorry that this wasn't more useful to you. I hope someone gives you an answer that is more useful to you. Are you familiar with Z3, with automated theorem provers, etc.? That might be starting point for more research. (This is one of the challenges of asking more than one question, in a post -- there is a risk you get an answer that answers only one of the questions and not the other -- and of asking a question that doesn't provide precise requirements or full context about what you're hoping for.) $\endgroup$
    – D.W. ♦
    Jan 7 at 22:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.