Publication:4809790
From MaRDI portal
zbMath1062.03003MaRDI QIDQ4809790
Publication date: 31 August 2004
sequent calculus; resolution; intuitionistic propositional logic; proof search; simply typed \(\lambda\)-calculus; intuitionistic natural deduction
03-02: Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03B70: Logic in computer science
03G30: Categorical logic, topoi
03F05: Cut-elimination and normal-form theorems
03F03: Proof theory in general (including proof-theoretic semantics)
03B20: Subsystems of classical logic (including intuitionistic logic)
03B40: Combinatory logic and lambda calculus
Related Items
Towards Ludics Programming: Interactive Proof Search, Semantical analysis of the logic of bunched implications, Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic, Proof and refutation in MALL as a game, A coinductive approach to proof search through typed lambda-calculi
Uses Software