2017/12/04 by Francesco Dagnino, Dagnino, Francesco
Computer Science · #03B70 #68Q55 #D.3.1 #F.3.1 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1712.01014
openalex publication_date 2017/12/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
After surveying classical results, we introduce a generalized notion of inference system to support structural recursion on non-well-founded data types. Besides axioms and inference rules with the usual meaning, a generalized inference system allows coaxioms, which are, intuitively, axioms which can only be applied "at infinite depth" in a proof tree. This notion nicely subsumes standard inference systems and their inductive and coinductive interpretation, while providing more flexibility. Indeed, the classical results can be extended to our generalized framework, interpreting recursive definitions as fixed points which are not necessarily the least, nor the greatest one. This allows formal reasoning in cases where the inductive and coinductive interpretation do not provide the intended meaning, or are mixed together.