scientific article; zbMATH DE number 7447752

MaRDI QIDQ3384900zbMATH OpenFDO

Authors Gabriel Ebner

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1810.07373, http://eptcs.web.cse.unsw.edu.au/paper.cgi?CLC2018.3

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• scientific article; zbMATH DE number 4087657
• Structure of proofs and the complexity of cut elimination
• scientific article; zbMATH DE number 1302630
• scientific article; zbMATH DE number 408808
• Cut-elimination and proof schemata
• Upper bound on the lengthening of proofs by cut elimination
• Cut Elimination in ε‐Calculi
• Optimizing proof search in model elimination
• scientific article; zbMATH DE number 7178366

Cites work

• A compact representation of proofs
• A symmetric lambda calculus for classical program extraction
• Algorithmic introduction of quantified cuts
• Applying tree languages in proof theory
• CERES in higher-order logic
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Cut-elimination and redundancy-elimination by resolution
• Expansion trees with cut
• Extracting Herbrand disjunctions by functional interpretation
• Extraction of expansion trees
• Herbrand's theorem as higher order recursion
• Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 4114622 (Why is no real title available?)
• scientific article; zbMATH DE number 3032487 (Why is no real title available?)
• Inductive theorem proving based on tree grammars
• Introducing quantified cuts in logic with equality
• On the complexity of proof deskolemization
• On the generation of quantified lemmas
• On the Infinitude of Primes
• Poincaré recurrence and number theory
• Practical foundations for programming languages
• Proof Transformation by CERES
• Strong normalisation of cut-elimination in classical logic
• System description: GAPT 2.0
• The consistency of arithmetics
• Towards Algorithmic Cut-Introduction
• Untersuchungen über das logische Schliessen. I

Cited in

(1)

• scientific article; zbMATH DE number 7178366 (Why is no real title available?)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384900)