Positive unit hyperresolution tableaux and their application to minimal model generation
From MaRDI portal
Recommendations
Cited in
(25)- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- First-order resolution methods for modal logics
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- Better paracoherent answer sets with less resources
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
- Efficient model generation through compilation
- Model building with ordered resolution: Extracting models from saturated clause sets
- Notions of sameness by default and their application to anaphora, vagueness, and uncertain reasoning
- A relevance restriction strategy for automated deduction
- Cautious reasoning in ASP via minimal models and unsatisfiable cores
- Constructing Bachmair-Ganzinger models
- Efficient model generation through compilation.
- A tableau calculus for minimal modal model generation
- ASP and subset minimality: enumeration, cautious reasoning and MUSes
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- Range-restricted and Horn interpolation through clausal tableaux
- Paracoherent answer set computation
- SHR tableaux -- a framework for automated model generation
- A tableau calculus for minimal model reasoning
- Minimal model generation with positive unit hyper-resolution tableaux
- Exploring theories with a model-finding assistant
- Blocking and other enhancements for bottom-up model generation methods
- An incremental algorithm for generating all minimal models
- Eliminating redundant search space on backtracking for forward chaining theorem proving
This page was built for publication: Positive unit hyperresolution tableaux and their application to minimal model generation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1581852)
