scientific article; zbMATH DE number 1222428

zbMath0924.03042MaRDI QIDQ4217953

Stephan Schmitt, Uwe Egly

Publication date: 11 November 1998

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

zbMATH Keywords

constructive proofcut ruleprogram synthesislength of proofssequent proofcut-free proof transformationmatrix proofmatrix-based theorem prover for first-order intuitionistic logicNUPRLproofs as programs paradigm

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Complexity of proofs (03F20)

Related Items (1)

Proof-search in type-theoretic languages: An introduction

Uses Software

• Nuprl

This page was built for publication: