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