scientific article
From MaRDI portal
Publication:2751380
zbMath1011.68130MaRDI QIDQ2751380
Publication date: 21 October 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (18)
Semantically-guided goal-sensitive reasoning: model representation ⋮ Prolog Technology Reinforcement Learning Prover ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Eliminating models during model elimination ⋮ Efficient Low-Level Connection Tableaux ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux ⋮ Craig interpolation with clausal first-order tableaux ⋮ Connection tableaux with lazy paramodulation ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ A Non-clausal Connection Calculus ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ Encoding First Order Proofs in SMT ⋮ Set of support, demodulation, paramodulation: a historical perspective
Uses Software
This page was built for publication:
