CERES in higher-order logic

DOI10.1016/J.APAL.2011.06.005MaRDI QIDQ716500zbMATH OpenOpenAlexFDO

Authors Stefan Hetzl, Alexander Leitsch, Daniel Weller

Publication date 22 September 2011

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

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

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)

Review text

Cut-elimination by resolution (CERES) for first-order logic [\textit{M. Baaz} et al., Lect. Notes Comput. Sci. 3452, 481--495 (2005; Zbl 1108.03305)] transforms the set of cut-formulas in a given proof \(\pi\) into a refutable formula \(R\). Given a resolution refutation of \(R\), cuts are sufficiently easily eliminated from \(\pi\). The extension \({\mathrm {CERES}}^\omega\) to higher-order logic described in the present paper is much more complicated. In particular, Skolemization involved in the first-order CERES is replaced here by a complicated mechanism of labels for quantifier rules in higher-order derivation, and a resolution calculus \(\mathcal{R}_{\mathrm{al}}\) used here is different from ordinary resolution \(\mathcal{R}\) for type theory [\textit{P. B. Andrews}, Stud. Log., Lond. 17, 63--81 (2008; Zbl 1226.03011)]. Completeness of \(\mathcal{R}_{\mathrm{al}}\) is conjectured, but not proved.

Recommendations

• CERES for first-order schemata
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proof Transformation by CERES
• Cut-elimination: syntax and semantics
• System Description: The Proof Transformation System CERES

Cites work

• A Clausal Approach to Proof Analysis in Second-Order Logic
• A compact representation of proofs
• A formulation of the simple theory of types
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Comparing approaches to resolution based higher-order theorem proving
• Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
• Cut-elimination and redundancy-elimination by resolution
• Herbrand Sequent Extraction
• Higher-order semantics and extensionality
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 932649 (Why is no real title available?)
• scientific article; zbMATH DE number 3090127 (Why is no real title available?)
• Intensional models for the theory of types
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Proofs from THE BOOK
• Resolution in type theory
• Theorem proving modulo
• Untersuchungen über das logische Schliessen. I
• Untersuchungen über das logische Schliessen. II

Cited in

(9)

• Cut-elimination: syntax and semantics
• Ceres in intuitionistic logic
• System description: GAPT 2.0
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• A Clausal Approach to Proof Analysis in Second-Order Logic
• Towards CERes in intuitionistic logic
• Proof Transformation by CERES
• CERES for first-order schemata
• Extraction of expansion trees

Describes a project that uses

Uses Software

• CERES

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

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