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 (11)

Unnamed Item ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ Unnamed Item ⋮ 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

• Nuprl
• ModLeanTAP
• Unnamed Item
• Unnamed Item

This page was built for publication: