Restricting backtracking in connection calculi
From MaRDI portal
Publication:3568228
DOI10.3233/AIC-2010-0464zbMath1205.68363OpenAlexW1826940506MaRDI QIDQ3568228
Publication date: 17 June 2010
Published in: AI Communications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.3233/aic-2010-0464
Related Items
\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 ⋮ Craig interpolation with clausal first-order tableaux ⋮ Cardinality Restrictions Within Description Logic Connection Calculi ⋮ On structures of regular standard contradictions in propositional logic ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ A Non-clausal Connection Calculus ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Specifying and Verifying Organizational Security Properties in First-Order Logic ⋮ Machine learning guidance for connection tableaux ⋮ A Connection Calculus for the Description Logic $$ {\mathcal{ALC}} $$ ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ From Schütte’s Formal Systems to Modern Automated Deduction
Uses Software
