scientific article; zbMATH DE number 1765687

zbMATH Open0988.68609MaRDI QIDQ4539627FDOQ4539627

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

Title of this publication is not available (Why is that?)

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

Mathematics Subject Classification ID

Cited In (10)

• Theorem prover for intuitionistic logic based on the inverse method
• 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

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)