Publication:4217953
From MaRDI portal
zbMath0924.03042MaRDI QIDQ4217953
Publication date: 11 November 1998
constructive proof; cut rule; program synthesis; length of proofs; sequent proof; cut-free proof transformation; matrix proof; matrix-based theorem prover for first-order intuitionistic logic; NUPRL; proofs as programs paradigm
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
03B35: Mechanization of proofs and logical operations
03F03: Proof theory in general (including proof-theoretic semantics)
03B20: Subsystems of classical logic (including intuitionistic logic)
03F20: Complexity of proofs
Related Items
Uses Software
