<p>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 <em>general case</em>. Using a FOL theorem prover covers any such query you could write in FOL... although of course, FOL is semi-decidable so it is not guaranteed that you can get an answer.</p>

<p>Your problem can be written in the <a href="http://www.cs.miami.edu/~tptp/" rel="nofollow noreferrer">TPTP language</a> as follows</p>

<pre><code>fof(listdef,axiom, 
  ![L] : (list(L) &lt;=&gt; 
        (null(L) | 
        (node(L) &amp; ?[Sub] : (list(Sub) &amp; next(L,Sub)))))).
fof(nodedefs,axiom, node(a) &amp; node(b) &amp; node(c) &amp; ~node(d)).
fof(nextdefs,axiom, next(a,b) &amp; next(b,c) &amp; next(c,d)).
fof(aislist,conjecture,list(a)).
</code></pre>

<p>and one can run a theorem prover on the problem. An easy way to do this would be to use the <a href="http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP" rel="nofollow noreferrer">online service</a>. Popular solvers include E and Vampire.</p>

<p>But, you will run it a problem as your problem does not contain the full specification of <code>node</code> and <code>null</code>. You are assuming they are disjoint and complete. If you add the following two axioms you get a proof that <code>a</code> is a list.</p>

<pre><code>fof(disjoint,axiom, ![L] : (~node(L) | ~null(L))).
fof(complete,axiom, ![L] : (node(L) | null(L))).
</code></pre>

<p>Most provers will negate the assertion <code>list(a)</code> and then use the definitions as rewrite rules to derive a contradiction.</p>

<p>It is worth commenting that List is a datatype and some theorem provers can reason directly with these e.g. Vampire, see <a href="https://dl.acm.org/citation.cfm?id=3009887" rel="nofollow noreferrer">here</a>.</p>

CC BY-SA 3.0
2017-10-13T16:55:52.723Z
+1 Thanks for your reply, it seems this is what I'm looking for. By *general case*, I mean when there is numerical operator in the formula, such as inductive definition for an AVL tree (there is numerical constraints about the height of branches). Can Vampire handle cases like that? I hope it is clear, but if it is not, I can write a definition for an AVL tree.
sean
CC BY-SA 3.0
2017-10-13T23:48:30.533Z
Vampire can handle mixtures of arithmetic, uninterpreted, and datatype symbols in a single formula. However, if the proof requires explicit induction then Vampire cannot currently support this (but watch this space). In general, I recommend using the TPTP syntax and trying out different solvers.
selig
CC BY-SA 3.0
2017-10-13T12:59:21.383Z
2017-10-13T12:59:21.383Z
selig
<p>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 equality cannot be considered a case of definition (what could be better depicted by $\triangleq$) since the predicate List appears on both sides of the equality. When creating a definition, the definiendum (in the left side of $\triangleq$) should not be mentioned in the definiens (right side of the $\triangleq$).</p>

<p>By FOL, are you referring to the so-called "first order programming logic" (a formal system specially designed for expressing recursive functions)? Since FOL cannot express transitive closure, I cannot think of a way to properly express recursion in FOL.</p>

CC BY-SA 3.0
2017-09-29T17:14:22.963Z
+1. I updated my question to to address your concerns. Thanks.
sean
CC BY-SA 3.0
2017-09-29T14:43:16.350Z
2017-09-29T14:43:16.350Z
Alessander Botti Benevides
<p>My setting is first-order logic. As an example, consider an inductive definition of a linked list:</p>

<blockquote>
  <p>$List(l)$ = $Null(l)$  $\vee~(Node(l) \wedge \exists sublist.   List(sublist) \wedge next(l,sublist))$</p>
</blockquote>

<p>This is straightforward, a list is a node connected to a sublist. Consider the following structure:</p>

<blockquote>
  <p>$Node(A)$, $Node(B)$, $Node(C)$, $Not\_A\_Node(D)$<br>
  $next(A,B)$, $next(B,C)$, $next(C,D)$<br>
  where $A, B, C, D$ are constants. </p>
</blockquote>

<p>How do I determine if $A$ is a list? If there is no numerical operator in the predicate, this is very similar to parsing context-free grammar, and I can use either bottom up or top down algorithm. But how to do in the general case?</p>

<p><strong>I'm asking for an automatic method.</strong> </p>

<p>If this is not a research-level question, please move it to an appropriate site. Thank you.</p>

<hr>

<p>@Alessander Botti Benevides: Thanks for your reply. The first equation is the definition. FOL with inductive definitions is described, for example, in this paper:</p>

<p>Cyclic Proofs for First-Order Logic with Inductive Definitions.James Brotherston. TABLEAUX 2005.<br>
<a href="http://www0.cs.ucl.ac.uk/staff/J.Brotherston/TABLEAUX05/cyclic_proofs_folind.pdf" rel="nofollow noreferrer">http://www0.cs.ucl.ac.uk/staff/J.Brotherston/TABLEAUX05/cyclic_proofs_folind.pdf</a></p>

<lo.logic><fl.formal-languages><grammars><logic-programming>
Determine if a structure is a model of an inductively defined predicate
sean
# Determine if a structure is a model of an inductively defined predicate

(Asked by: username_0 on 2017-09-25)

My setting is first-order logic. As an example, consider an inductive definition of a linked list:

> $List(l)$ = $Null(l)$ $\vee~(Node(l) \wedge \exists sublist. List(sublist) \wedge next(l,sublist))$

This is straightforward, a list is a node connected to a sublist. Consider the following structure:

> $Node(A)$, $Node(B)$, $Node(C)$, $Not\\_A\\_Node(D)$  
> $next(A,B)$, $next(B,C)$, $next(C,D)$  
> where $A, B, C, D$ are constants.

How do I determine if $A$ is a list? If there is no numerical operator in the predicate, this is very similar to parsing context-free grammar, and I can use either bottom up or top down algorithm. But how to do in the general case?

**I'm asking for an automatic method.**

If this is not a research-level question, please move it to an appropriate site. Thank you.

---

@username_2: Thanks for your reply. The first equation is the definition. FOL with inductive definitions is described, for example, in this paper:

Cyclic Proofs for First-Order Logic with Inductive Definitions.James Brotherston. TABLEAUX 2005.  
<http://www0.cs.ucl.ac.uk/staff/J.Brotherston/TABLEAUX05/cyclic_proofs_folind.pdf>

**Tags:** lo.logic, fl.formal-languages, grammars, logic-programming


---

## 2 answers

### Answer by username_1 on 2017-10-13. Score: 1 | Accepted answer

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 in FOL... although of course, FOL is semi-decidable so it is not guaranteed that you can get an answer.
Your problem can be written in the TPTP language as follows
fof(listdef,axiom, 
  ![L] : (list(L) <=> 
        (null(L) | 
        (node(L) & ?[Sub] : (list(Sub) & next(L,Sub)))))).
fof(nodedefs,axiom, node(a) & node(b) & node(c) & ~node(d)).
fof(nextdefs,axiom, next(a,b) & next(b,c) & next(c,d)).
fof(aislist,conjecture,list(a)).

and one can run a theorem prover on the problem. An easy way to do this would be to use the online service. Popular solvers include E and Vampire.
But, you will run it a problem as your problem does not contain the full specification of node and null. You are assuming they are disjoint and complete. If you add the following two axioms you get a proof that a is a list.
fof(disjoint,axiom, ![L] : (~node(L) | ~null(L))).
fof(complete,axiom, ![L] : (node(L) | null(L))).

Most provers will negate the assertion list(a) and then use the definitions as rewrite rules to derive a contradiction.
It is worth commenting that List is a datatype and some theorem provers can reason directly with these e.g. Vampire, see here.

> **Comments:**
> **username_0**: +1 Thanks for your reply, it seems this is what I'm looking for. By *general case*, I mean when there is numerical operator in the formula, such as inductive definition for an AVL tree (there is numerical constraints about the height of branches). Can Vampire handle cases like that? I hope it is clear, but if it is not, I can write a definition for an AVL tree.  
> **username_1**: Vampire can handle mixtures of arithmetic, uninterpreted, and datatype symbols in a single formula. However, if the proof requires explicit induction then Vampire cannot currently support this (but watch this space). In general, I recommend using the TPTP syntax and trying out different solvers.  

---

### Answer by username_2 on 2017-09-29. Score: 4

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 equality cannot be considered a case of definition (what could be better depicted by $\triangleq$) since the predicate List appears on both sides of the equality. When creating a definition, the definiendum (in the left side of $\triangleq$) should not be mentioned in the definiens (right side of the $\triangleq$).

By FOL, are you referring to the so-called "first order programming logic" (a formal system specially designed for expressing recursive functions)? Since FOL cannot express transitive closure, I cannot think of a way to properly express recursion in FOL.

> **Comments:**
> **username_0**: +1. I updated my question to to address your concerns. Thanks.  

---

