A complete cyclic proof system for inductive entailments in first order logic. (English) Zbl 1416.03027

Iosif, Radu; Serban, Cristina

Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 435-453 (2018).

Summary: In this paper, we develop a cyclic proof system for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions are quantifier-free formulae of first order logic. The proof system consists of a small set of inference rules, inspired by a top-down language inclusion algorithm for tree automata [L. Holík et al., Lect. Notes Comput. Sci. 6996, 243–258 (2011; Zbl 1348.68105)]. We show the proof system to be sound, in general, and complete, under certain semantic restrictions involving the set of constraints in the inductive system. Moreover, we investigate the computational complexity of checking these restrictions, when the function symbols in the logic are given the canonical Herbrand interpretation.
For the entire collection see [Zbl 1407.68021].

MSC:

03F07	Structure of proofs
03D05	Automata and formal grammars in connection with logical questions

Keywords:

antichain-based tree automata language inclusion; cyclic proofs; inductive definitions; infinite descent