scientific article; zbMATH DE number 1543301

zbMath0961.68118MaRDI QIDQ4520768

Jens Otten, Christoph Kreitz

Publication date: 27 February 2001

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

linear logicintuitionistic logicmodal logicsproof searchclassical logic

Mathematics Subject Classification ID

Related Items

Unnamed Item, Practical Proof Search for Coq by Type Inhabitation, Innovations in computational type theory using Nuprl, IeanCOP: lean connection-based theorem proving, Incremental variable splitting, leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions), A Non-clausal Connection Calculus, Specifying and Verifying Organizational Security Properties in First-Order Logic, nanoCoP: A Non-clausal Connection Prover, Hypothesis finding with proof theoretical appropriateness criteria

Uses Software

• Coq
• SETHEO
• Nuprl
• ModLeanTAP