Positive unit hyperresolution tableaux and their application to minimal model generation
From MaRDI portal
Publication:1581852
DOI10.1023/A:1006291616338zbMath0960.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
Related Items
SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, Exploring Theories with a Model-Finding Assistant, Cautious reasoning in ASP via minimal models and unsatisfiable cores, Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, ASP and subset minimality: enumeration, cautious reasoning and MUSes, Better Paracoherent Answer Sets with Less Resources, Model building with ordered resolution: Extracting models from saturated clause sets, 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, Paracoherent answer set computation, First-Order Resolution Methods for Modal Logics, Blocking and other enhancements for bottom-up model generation methods, A Tableau Calculus for Minimal Modal Model Generation, Notions of sameness by default and their application to anaphora, vagueness, and uncertain reasoning, Completeness of hyper-resolution via the semantics of disjunctive logic programs, A relevance restriction strategy for automated deduction
Uses Software
