Ceres in intuitionistic logic

DOI10.1016/J.APAL.2017.04.001MaRDI QIDQ2363201zbMATH OpenOpenAlexFDO

Authors Giselle Reis, Simon Wolfsteiner, David M. Cerna, Alexander Leitsch

Publication date 13 July 2017

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.2017.04.001

zbMATH Keywords

intuitionistic logiccut-eliminationCERESproof resolution

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Recommendations

• Towards CERes in intuitionistic logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Methods of cut-elimination
• Logic for Programming, Artificial Intelligence, and Reasoning
• Cut-elimination: syntax and semantics

Cites work

• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• CERES in higher-order logic
• CERES: An analysis of Fürstenberg's proof of the infinity of primes
• Computer Science Logic
• Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
• Cut-elimination and proof schemata
• Cut-elimination and redundancy-elimination by resolution
• Cut-elimination: syntax and semantics
• Linear algebra and geometry. Translated from the Russian by David Kramer and Lena Nekludova
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Lower Bounds on Herbrand's Theorem
• Methods of cut-elimination
• Towards CERes in intuitionistic logic

Cited in

(3)

• Cut-elimination: syntax and semantics
• Towards CERes in intuitionistic logic
• Logic for Programming, Artificial Intelligence, and Reasoning

Describes a project that uses

Uses Software

• CERES

This page was built for publication: Ceres in intuitionistic logic

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