Related papers: Induction and Co-induction in Sequent Calculus
Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing…
An inductive inference system for proving validity of formulas in the initial algebra $T_{\mathcal{E}}$ of an order-sorted equational theory $\mathcal{E}$ is presented. It has 20 inference rules, but only 9 of them require user interaction;…
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…
This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the…
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of…
We introduce a generalized logic programming paradigm where programs, consisting of facts and rules with the usual syntax, can be enriched by co-facts, which syntactically resemble facts but have a special meaning. As in coinductive logic…
Deep inference is a proof theoretic methodology that generalizes the standard notion of inference of the sequent calculus, whereby inference rules become applicable at any depth inside logical expressions. Deep inference provides more…
We introduce a non-wellfounded proof system for intuitionistic logic extended with inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. We explore the…
The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes…
Mathematical induction is a fundamental tool in computer science and mathematics. Henkin initiated the study of formalization of mathematical induction restricted to the setting when the base case B is set to singleton set containing 0 and…
Large language models make remarkable progress in reasoning capabilities. Existing works focus mainly on deductive reasoning tasks (e.g., code and math), while another type of reasoning mode that better aligns with human learning, inductive…
Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than…
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The reason for that is that in first-order logic induction requires…
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search…
In this paper, we establish the foundations of a novel logical framework for the {\pi}-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic interpretation of logic programming, we represent…
Inductive definitions are an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic FO with general non-monotone inductive definitions. Most existing proof systems for inductive definitions impose…
Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations including decidability,…
As mathematical induction is applied to prove statements on natural numbers, {\it continuous induction} (or, {\it real induction}) is a tool to prove some statements in real analysis.(Although, this comparison is somehow an overstatement.)…
We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit induction proof, is an instance of Noetherian induction.…