Restricting backtracking in connection calculi
From MaRDI portal
Publication:3568228
DOI10.3233/AIC-2010-0464zbMath1205.68363MaRDI 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
From Schütte’s Formal Systems to Modern Automated Deduction, Cardinality Restrictions Within Description Logic Connection Calculi, Machine learning guidance for connection tableaux, \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, Craig interpolation with clausal first-order tableaux, A Connection Calculus for the Description Logic $$ {\mathcal{ALC}} $$, nanoCoP: A Non-clausal Connection Prover, A Non-clausal Connection Calculus, MaLeCoP Machine Learning Connection Prover, Specifying and Verifying Organizational Security Properties in First-Order Logic, Efficient Low-Level Connection Tableaux, leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
Uses Software