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.