Positive unit hyperresolution tableaux and their application to minimal model generation
From MaRDI portal
DOI10.1023/A:1006291616338zbMATH Open0960.03006OpenAlexW2150903551MaRDI QIDQ1581852FDOQ1581852
Authors: François Bry, Adnan Yahya 
Publication date: 6 February 2001
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1006291616338
Recommendations
Cited In (25)
- Efficient model generation through compilation.
- Blocking and other enhancements for bottom-up model generation methods
- A tableau calculus for minimal model reasoning
- Minimal model generation with positive unit hyper-resolution tableaux
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- An incremental algorithm for generating all minimal models
- Better paracoherent answer sets with less resources
- ASP and subset minimality: enumeration, cautious reasoning and MUSes
- Paracoherent answer set computation
- Exploring theories with a model-finding assistant
- Representing and building models for decidable subclasses of equational clausal logic
- Some techniques for proving termination of the hyperresolution calculus
- A tableau calculus for minimal modal model generation
- Notions of sameness by default and their application to anaphora, vagueness, and uncertain reasoning
- Model building with ordered resolution: Extracting models from saturated clause sets
- Cautious reasoning in ASP via minimal models and unsatisfiable cores
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- SHR tableaux -- a framework for automated model generation
- Efficient model generation through compilation
- First-order resolution methods for modal logics
- Range-restricted and Horn interpolation through clausal tableaux
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
- A relevance restriction strategy for automated deduction
- Constructing Bachmair-Ganzinger models
Uses Software
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)
