Pages that link to "Item:Q3103982"

The following pages link to Sequent calculi for induction and infinite descent (Q3103982):

Displaying 49 items.

• The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics (Q383070) (← links)
• Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
• On the proof theory of the modal mu-calculus (Q1005937) (← links)
• Inductive proof search modulo (Q1037404) (← links)
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs (Q1798782) (← links)
• Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps (Q2039937) (← links)
• Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
• Integrating induction and coinduction via closure operators and proof cycles (Q2096458) (← links)
• Cyclic proofs, hypersequents, and transitive closure logic (Q2104539) (← links)
• Uniform interpolation from cyclic proofs: the case of modal mu-calculus (Q2142087) (← links)
• Cyclic hypersequent calculi for some modal logics with the master modality (Q2142089) (← links)
• Historical and foundational details on the method of infinite descent: every prime number of the form \(4n+1\) is the sum of two squares (Q2151525) (← links)
• Asynchronous unfold/fold transformation for fixpoint logic (Q2163155) (← links)
• Herzberger's limit rule with labelled sequent calculus (Q2193976) (← links)
• Automated repair of heap-manipulating programs using deductive synthesis (Q2234087) (← links)
• Inductive theorem proving based on tree grammars (Q2344621) (← links)
• Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
• Schematic refutations of formula schemata (Q2666952) (← links)
• Schematic Cut Elimination and the Ordered Pigeonhole Principle (Q2817924) (← links)
• Extracting Proofs from Tabled Proof Search (Q2938048) (← links)
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic (Q2961583) (← links)
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic (Q2988374) (← links)
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System (Q2988375) (← links)
• (Q3121528) (← links)
• Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut (Q3305560) (← links)
• (Q3384901) (← links)
• Cut-Elimination and Proof Schemata (Q3455184) (← links)
• Descente Infinie + Deduction (Q4809499) (← links)
• Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto (Q4913999) (← links)
• Geometric Rules in Infinitary Logic (Q5020172) (← links)
• (Q5028421) (← links)
• Soundness Conditions for Big-Step Semantics (Q5041092) (← links)
• Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent (Q5079741) (← links)
• (Q5079760) (← links)
• (Q5089276) (← links)
• The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them (Q5140030) (← links)
• (Q5140266) (← links)
• Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
• (Q5208872) (← links)
• (Q5227521) (← links)
• Coinduction in Flow: The Later Modality in Fibrations (Q5875348) (← links)
• Cyclic hypersequent system for transitive closure logic (Q6050767) (← links)
• A proof procedure for separation logic with inductive definitions and data (Q6053843) (← links)
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs (Q6059221) (← links)
• Completeness of cyclic proofs for symbolic heaps with inductive definitions (Q6536318) (← links)
• A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points (Q6541152) (← links)
• Restriction on cut rule in cyclic-proof system for symbolic heaps (Q6633582) (← links)
• Cyclic implicit complexity (Q6649449) (← links)
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs (Q6649500) (← links)