Publication:4809790

zbMath1062.03003MaRDI QIDQ4809790

Eike Ritter, David J. Pym

Publication date: 31 August 2004

zbMATH Keywords

sequent calculus; resolution; intuitionistic propositional logic; proof search; simply typed \(\lambda\)-calculus; intuitionistic natural deduction

Mathematics Subject Classification ID

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, Proof and refutation in MALL as a game

Uses Software

• Pesca