Paper Info
Title
Complete Cyclic Proof Systems for Inductive Entailments.
Abstract
In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions belong to the quantifier-free fragments of (i) First Order Logic with the canonical Herbrand interpretation and (ii) Separation Logic, respectively. Inspired by classical automata-theoretic techniques of proving language inclusion between tree automata, we give a small set of inference rules, that are proved to be sound and complete, under certain semantic restrictions, involving the set of constraints in the inductive system. Moreover, we investigate the decidability and computational complexity of these restrictions for all the logical fragments considered and provide a proof search semi-algorithm that becomes a decision procedure for the entailment problem, for those systems that fulfill the restrictions.
Year
Venue
Field
2017
arXiv: Logic in Computer Science
Discrete mathematics,Separation logic,Logical consequence,Algorithm,Decidability,First-order logic,Herbrand interpretation,Rule of inference,Recursion,Mathematics,Computational complexity theory
DocType
Volume
Citations 
Journal
abs/1707.02415
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Radu Iosif148342.44
Cristina Serban242.19