Validating Back-links of FOL$_{\mbox{\normalsize ID}}$ Cyclic Pre-proofs

Author: Sorin Stratulat

Paper Information

Title:Validating Back-links of FOL$_{\mbox{\normalsize ID}}$ Cyclic Pre-proofs
Authors:Sorin Stratulat
Proceedings:CL&C Full papers and abstracts
Editor: Stefano Berardi
Keywords:mechanical reasoning, first-order logic with inductive definitions, induction reasoning, cyclic induction

ABSTRACT. Cyclic pre-proofs can be represented as sets of finite tree derivations with back-links. In the frame of the first-order logic with inductive definitions (FOL$_{\mbox{\scriptsize ID}}$), the nodes of the tree derivations are labelled by sequents and the back-links connect particular terminal nodes, referred to as \emph{buds}, to other nodes labelled by a same sequent. However, only some back-links can constitute sound pre-proofs. Previously, it has been shown that special ordering and derivability conditions, defined along the minimal cycles of the digraphs representing particular normal forms of cyclic pre-proofs, are sufficient for validating the back-links. In that approach, a same constraint could be checked several times when processing different minimal cycles, hence one may require additional recording mechanisms to avoid redundant computation in order to downgrade the time complexity to polynomial.

We present a new approach that does not need to process minimal cycles. It based on a normal form that allows to define the validation conditions by taking into account only the root-bud paths from the non-singleton strongly connected components existing in the digraphs.

Talk:Jul 07 11:45 (Session 26A)