Sequent calculi for induction and infinite descent
From MaRDI portal
Publication:3103982
DOI10.1093/logcom/exq052zbMath1242.03084OpenAlexW1999823887MaRDI QIDQ3103982
James Brotherston, Alex K. Simpson
Publication date: 19 December 2011
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://www.pure.ed.ac.uk/ws/files/12304236/bs_journal.pdf
Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items
Soundness and completeness proofs by coinductive methods, Soundness Conditions for Big-Step Semantics, Uniform interpolation from cyclic proofs: the case of modal mu-calculus, Cyclic hypersequent calculi for some modal logics with the master modality, Cut-Elimination and Proof Schemata, Unnamed Item, Historical and foundational details on the method of infinite descent: every prime number of the form \(4n+1\) is the sum of two squares, Asynchronous unfold/fold transformation for fixpoint logic, Unnamed Item, Extracting Proofs from Tabled Proof Search, Schematic refutations of formula schemata, The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics, Cyclic hypersequent system for transitive closure logic, A proof procedure for separation logic with inductive definitions and data, Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs, A logical framework with higher-order rational (circular) terms, Circular (Yet Sound) Proofs in Propositional Logic, Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, Polarized subtyping, Unnamed Item, Cyclic Arithmetic Is Equivalent to Peano Arithmetic, Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System, Unnamed Item, The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them, Coinduction in Flow: The Later Modality in Fibrations, Automated repair of heap-manipulating programs using deductive synthesis, Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut, Mechanically certifying formula-based Noetherian induction reasoning, Unnamed Item, Unnamed Item, Unnamed Item, Automated Cyclic Entailment Proofs in Separation Logic, Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps, Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs, On the proof theory of the modal mu-calculus, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent, Schematic Cut Elimination and the Ordered Pigeonhole Principle, Non-well-founded deduction for induction and coinduction, Unnamed Item, Inductive proof search modulo, Integrating induction and coinduction via closure operators and proof cycles, Inductive theorem proving based on tree grammars, Cyclic proofs, hypersequents, and transitive closure logic, Geometric Rules in Infinitary Logic
