Blocking and other enhancements for bottom-up model generation methods
From MaRDI portal
Publication:2303239
DOI10.1007/s10817-019-09515-1zbMath1468.68279OpenAlexW2919937788MaRDI QIDQ2303239
Peter Baumgartner, Renate A. Schmidt
Publication date: 3 March 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-019-09515-1
Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Craig interpolation with clausal first-order tableaux, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), Possible models computation and revision -- a practical approach
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A bi-intuitionistic modal logic: foundations and automation
- On deciding satisfiability by theorem proving with speculative inferences
- Computing finite models by reduction to function-free clause logic
- A new methodology for developing deduction methods
- Terminating tableau systems for hybrid logic with difference and converse
- Proof methods for modal and intuitionistic logics
- Critical pair criteria for completion
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Resolution methods for the decision problem
- A tableau prover for domain minimization
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- Computing answers with model elimination
- A calculus combining resolution and enumeration for building finite models
- Hyperresolution for guarded formulae
- Positive unit hyperresolution tableaux and their application to minimal model generation
- Using resolution for testing modal satisfiability and building models
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- A tableau decision procedure for \(\mathcal{SHOIQ}\)
- Automated model building
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- A Tableau Calculus for Minimal Modal Model Generation
- Computing Minimal Models Modulo Subset-Simulation for Modal Logics
- A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$
- System Description: E 1.8
- The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation
- Tableau-based Decision Procedures for Hybrid Logic
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- Hyper Tableaux with Equality
- System Description: E- KRHyper
- System Description: Spass Version 3.0
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
- A description logic with transitive and inverse roles and role hierarchies
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Practical reasoning for very expressive description logics
- Resolution-based methods for modal logics
- Tableaux for diagnosis applications
- Hyperresolution and automated model building
- MACE4 and SEM: A Comparison of Finite Model Generators
- Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving
- Hyper tableaux
- Computer Science Logic
- Computer Science Logic
- Using tableau to decide description logics with full role negation and identity
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
- A maximal-literal unit strategy for horn clauses
- Automated Synthesis of Tableau Calculi
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- An overview of tableau algorithms for description logics
