scientific article; zbMATH DE number 1765687

MaRDI QIDQ4539627zbMATH OpenFDO

Authors Stephan Schmitt, L. Lorigo, Christoph Kreitz, Aleksey Nogin

Publication date 10 July 2002

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2083/20830421

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 3870635
• Connection-driven inductive theorem proving
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A light-weight integration of automated and interactive theorem proving
• A survey of interactive theorem proving
• IeanCOP: lean connection-based theorem proving
• scientific article; zbMATH DE number 2177623
• scientific article; zbMATH DE number 1552511
• scientific article; zbMATH DE number 4094863
• scientific article; zbMATH DE number 1543301

Cited in

(11)

• Theorem prover for intuitionistic logic based on the inverse method
• Subformula linking for intuitionistic logic with application to type theory
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• The ILTP problem library for intuitionistic logic
• JProver
• Innovations in computational type theory using Nuprl
• Practical Proof Search for Coq by Type Inhabitation
• A Non-clausal Connection Calculus
• Hammer for Coq: automation for dependent type theory
• The Lean theorem prover (system description)
• nanoCoP: a non-clausal connection prover

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4539627)