scientific article
From MaRDI portal
Publication:3384900
Publication date: 17 December 2021
Full work available at URL: https://arxiv.org/abs/1810.07373
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Algorithmic introduction of quantified cuts
- Extraction of expansion trees
- CERES in higher-order logic
- CERES: An analysis of Fürstenberg's proof of the infinity of primes
- A compact representation of proofs
- Untersuchungen über das logische Schliessen. I
- A symmetric lambda calculus for classical program extraction
- Herbrand's theorem as higher order recursion
- Inductive theorem proving based on tree grammars
- On the generation of quantified lemmas
- Extracting Herbrand disjunctions by functional interpretation
- Practical Foundations for Programming Languages
- System Description: GAPT 2.0
- Applying Tree Languages in Proof Theory
- Towards Algorithmic Cut-Introduction
- On the complexity of proof deskolemization
- On the Infinitude of Primes
- Introducing Quantified Cuts in Logic with Equality
- Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken
- Poincaré recurrence and number theory
- Expansion trees with cut
- Proof Transformation by CERES
- The consistency of arithmetics
- Cut-elimination and redundancy-elimination by resolution
This page was built for publication: