JProver: Integrating connection-based theorem proving into interactive proof assistants

DOI10.1007/3-540-45744-5_34MaRDI QIDQ4539627zbMATH OpenFDO

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

Publication date 10 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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)

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

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: JProver: Integrating connection-based theorem proving into interactive proof assistants

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