Blocking and other enhancements for bottom-up model generation methods
From MaRDI portal
Publication:2303239
DOI10.1007/S10817-019-09515-1zbMATH Open1468.68279OpenAlexW2919937788MaRDI QIDQ2303239FDOQ2303239
Authors: 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
Recommendations
Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Title not available (Why is that?)
- Title not available (Why is that?)
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- System description: E 1.8
- A tableau prover for domain minimization
- System Description: E- KRHyper
- Resolution theorem proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Title not available (Why is that?)
- Practical reasoning for very expressive description logics
- Title not available (Why is that?)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Automated model building
- Combining superposition, sorts and splitting
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- On deciding satisfiability by theorem proving with speculative inferences
- Title not available (Why is that?)
- Bugs, moles and skeletons: symbolic reasoning for software development
- A bi-intuitionistic modal logic: foundations and automation
- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- A description logic with transitive and inverse roles and role hierarchies
- Axiomatic and tableau-based reasoning for \(Kt (H, R)\)
- Using tableau to decide description logics with full role negation and identity
- Automated synthesis of tableau calculi
- Critical pair criteria for completion
- Paramodulation-based theorem proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- An overview of tableau algorithms for description logics
- Proof methods for modal and intuitionistic logics
- Single step tableaux for modal logics. Computational properties, complexity and methodology
- System Description: Spass Version 3.0
- Computer Science Logic
- Computer Science Logic
- Terminating tableau systems for hybrid logic with difference and converse
- A tableau decision procedure for \(\mathcal{SHOIQ}\)
- A maximal-literal unit strategy for horn clauses
- Title not available (Why is that?)
- Resolution-based methods for modal logics
- Tableau-based Decision Procedures for Hybrid Logic
- Title not available (Why is that?)
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- Hyperresolution and automated model building
- Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
- Positive unit hyperresolution tableaux and their application to minimal model generation
- Title not available (Why is that?)
- A new methodology for developing deduction methods
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Hyper tableaux
- Resolution methods for the decision problem
- A calculus combining resolution and enumeration for building finite models
- Hyperresolution for guarded formulae
- Using resolution for testing modal satisfiability and building models
- Hyper Tableaux with Equality
- Computing finite models by reduction to function-free clause logic
- Computing answers with model elimination
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
- The hyper tableaux calculus with equality and an application to finite model computation
- Tableaux for diagnosis applications
- A tableau calculus for minimal modal model generation
- Deductive systems and the decidability problem for hybrid logics
- Computing minimal models modulo subset-simulation for modal logics
- A refined tableau calculus with controlled blocking for the description logic \(\mathcal{SHOI}\)
- Nominal substitution at work with the global and converse modalities
- MACE4 and SEM: a comparison of finite model generators
- Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving
Cited In (8)
- Efficient model generation through compilation.
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Possible models computation and revision -- a practical approach
- Model generation with Boolean constraints
- Craig interpolation with clausal first-order tableaux
- Range-restricted and Horn interpolation through clausal tableaux
Uses Software
This page was built for publication: Blocking and other enhancements for bottom-up model generation methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2303239)
