scientific article; zbMATH DE number 2095713

zbMath1062.03003MaRDI QIDQ4809790

Eike Ritter, David J. Pym

Publication date: 31 August 2004

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

sequent calculusresolutionintuitionistic propositional logicproof searchsimply typed \(\lambda\)-calculusintuitionistic natural deduction

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items (5)

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 ⋮ Towards Ludics Programming: Interactive Proof Search

Uses Software

• Pesca

This page was built for publication: