1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ +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. $\endgroup$ – qsp Oct 13 '17 at 16:55
  • 1
    $\begingroup$ 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. $\endgroup$ – selig Oct 13 '17 at 23:48
4
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ +1. I updated my question to to address your concerns. Thanks. $\endgroup$ – qsp Sep 29 '17 at 17:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.