scientific article; zbMATH DE number 1543301

MaRDI QIDQ4520768zbMATH OpenFDO

Authors Christoph Kreitz, Jens Otten

Publication date 27 February 2001

Full work available at URL http://www.jucs.org/jucs_5_3/connection_based_theorem_proving

zbMATH Keywords

classical logicintuitionistic logiclinear logicmodal logicsproof search

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 49746
• A family of goal directed theorem provers based on conjunction and implication. I
• Connection-based proof construction in linear logic
• Non-clausal connection calculi for non-classical logics
• On the intuitionistic force of classical search (extended abstract)

Cited in

(24)

• A family of goal directed theorem provers based on conjunction and implication. I
• IeanCOP: lean connection-based theorem proving
• A vision for automated deduction rooted in the connection method
• Non-clausal connection calculi for non-classical logics
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• Proof-search and proof nets in mixed linear logic
• Proof reconstruction in classical and nonclassical logics (Diss., TU Darmstadt, 1999)
• Connections in nonclassical logics
• nanoCoP: a non-clausal connection prover
• A Non-clausal Connection Calculus
• Specifying and verifying organizational security properties in first-order logic
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• scientific article; zbMATH DE number 4094863 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• Incremental variable splitting
• scientific article; zbMATH DE number 1765687 (Why is no real title available?)
• T-string unification: unifying prefixes in non-classical proof methods
• scientific article; zbMATH DE number 3992946 (Why is no real title available?)
• Practical Proof Search for Coq by Type Inhabitation
• Connection-based proof construction in linear logic
• scientific article; zbMATH DE number 6290320 (Why is no real title available?)
• Connection calculus theorem proving with multiple built-in theories
• Hypothesis finding with proof theoretical appropriateness criteria
• Innovations in computational type theory using Nuprl

Describes a project that uses

Uses Software

• Nuprl
• Coq
• SETHEO
• ModLeanTAP

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 Q4520768)