System Description: GAPT 2.0

DOI10.1007/978-3-319-40229-1_20zbMath1475.68433OpenAlexW2505251503MaRDI QIDQ2817928

Martin Riener, Sebastian Zivota, Gabriel Ebner, Simon Wolfsteiner, Stefan Hetzl, Giselle Reis

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40229-1_20

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ On the generation of quantified lemmas ⋮ Unnamed Item ⋮ Extraction of expansion trees ⋮ Scalable fine-grained proofs for formula processing ⋮ GAPT ⋮ Expansion trees with cut ⋮ Complexity of translations from resolution to sequent calculus

Uses Software

• TPTP
• CERES
• ProofTool
• OpenTheory

Cites Work

• Unnamed Item
• Algorithmic introduction of quantified cuts
• CERES in higher-order logic
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• A compact representation of proofs
• Inductive theorem proving based on tree grammars
• Understanding Resolution Proofs through Herbrand’s Theorem
• Towards Algorithmic Cut-Introduction
• Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)
• The TPTP World – Infrastructure for Automated Reasoning
• Introducing Quantified Cuts in Logic with Equality
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Resolution in type theory
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: System Description: GAPT 2.0