Positive unit hyperresolution tableaux and their application to minimal model generation
From MaRDI portal
Publication:1581852
DOI10.1023/A:1006291616338zbMATH Open0960.03006OpenAlexW2150903551MaRDI QIDQ1581852
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
Cited In (19)
- Blocking and other enhancements for bottom-up model generation methods
- 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
- ASP and subset minimality: enumeration, cautious reasoning and MUSes
- Paracoherent answer set computation
- 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
- First-Order Resolution Methods for Modal Logics
- 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
- Exploring Theories with a Model-Finding Assistant
- Completeness of hyper-resolution via the semantics of disjunctive logic programs
- Better Paracoherent Answer Sets with Less Resources
- Range-restricted and Horn interpolation through clausal tableaux
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
- A relevance restriction strategy for automated deduction
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)
