Skip to main content
4 votes

Determine if a structure is a model of an inductively defined predicate

What do you mean by the equality in your first formula? In first-order logic (FOL) with equality, one can only apply the equality operator to a couple of terms, not to formulae. Also, your use of ...
Alessander Botti Benevides's user avatar
3 votes

In logic programming, what would a language with second-order model theory gain?

An actual second-order logic programming language would allow you to use second-order quantifiers in a computationally meaningful way. Second-order logic without quantifiers ranging over second-order ...
Andrej Bauer's user avatar
  • 29.2k
2 votes

resolution based theorem prover for temporal logic

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. ...
Neel Krishnaswami's user avatar
1 vote

How to solve an unification problem on $\mathbb{N}$?

I have concluded that one cannot add both + and × in the λProlog programming language with their arithmetic semantics since the decision problem is undeciable. Because if it was decidable then Hilbert'...
Kijeong Lim's user avatar
1 vote

Determine if a structure is a model of an inductively defined predicate

If your setting is FOL then why not just use a FOL theorem prover. What is unclear from your question is what you mean by general case. Using a FOL theorem prover covers any such query you could write ...
selig's user avatar
  • 333

Only top scored, non community-wiki answers of a minimum length are eligible