Determine if a structure is a model of an inductively defined predicate 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
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.