Share Your Experience: Take the 2024 Developer Survey

# Tag Info

### 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 ...

### 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 ...
• 29.2k

### 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. ...
• 32.6k
1 vote
Accepted

### 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'...
1 vote
Accepted

### 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 ...
• 333

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