CERES in higher-order logic

DOI10.1016/J.APAL.2011.06.005zbMath1259.03071OpenAlexW2156662803MaRDI QIDQ716500

Daniel Weller, Alexander Leitsch, Stefan Hetzl

Publication date: 22 September 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.06.005

zbMATH Keywords

cut eliminationhigher-order logicresolution

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Related Items (5)

Ceres in intuitionistic logic ⋮ Unnamed Item ⋮ Extraction of expansion trees ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ System Description: GAPT 2.0

Uses Software

• CERES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• A compact representation of proofs
• Theorem proving modulo
• Untersuchungen über das logische Schliessen. I
• Untersuchungen über das logische Schliessen. II
• Comparing approaches to resolution based higher-order theorem proving
• Intensional models for the theory of types
• A Clausal Approach to Proof Analysis in Second-Order Logic
• Higher-order semantics and extensionality
• Herbrand Sequent Extraction
• Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
• Resolution in type theory
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• A formulation of the simple theory of types
• Proofs from THE BOOK
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: CERES in higher-order logic