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.
$\endgroup$
3
  • 1
    $\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.
    Commented Jan 7, 2023 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$ Commented Jan 7, 2023 at 22:06
  • $\begingroup$ Since the bot bumped this question, it might be better asked in Proof Assistants. $\endgroup$
    – Pseudonym
    Commented Jun 7, 2023 at 2:37

1 Answer 1

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.

$\endgroup$
2
  • $\begingroup$ I was hoping and assuming there was something like DPLL(T) that resolves n-ary predicates. $\endgroup$ Commented Jan 7, 2023 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.
    Commented Jan 7, 2023 at 22:34

Your Answer

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

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