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

Question

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.

---

@Alessander Botti Benevides: 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

Answer 1

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.

Answer 2

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.