Blocking and Other Enhancements for Bottom-Up Model Generation Methods
From MaRDI portal
Publication:3613405
DOI10.1007/11814771_11zbMath1222.68357arXiv1611.09014OpenAlexW1534896904MaRDI QIDQ3613405
Peter Baumgartner, Renate A. Schmidt
Publication date: 12 March 2009
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1611.09014
Related Items
A bi-intuitionistic modal logic: foundations and automation, Exploring Theories with a Model-Finding Assistant, Modal Tableau Systems with Blocking and Congruence Closure, Simulation and Synthesis of Deduction Calculi, On deciding satisfiability by theorem proving with speculative inferences, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Using tableau to decide description logics with full role negation and identity, Superposition for Bounded Domains, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, First-Order Resolution Methods for Modal Logics, Optimized Description Logic Reasoning via Core Blocking, Computing finite models by reduction to function-free clause logic, Blocking and other enhancements for bottom-up model generation methods, A new methodology for developing deduction methods
Uses Software
