Positive unit hyperresolution tableaux and their application to minimal model generation

DOI10.1023/A:1006291616338MaRDI QIDQ1581852zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

first-order clausesHerbrand modelsminimal modelmodel generationproof theorytableau

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Minimal model generation with positive unit hyper-resolution tableaux
• scientific article; zbMATH DE number 1341481
• Hyperresolution and automated model building
• A tableau calculus for minimal model reasoning
• A tableau calculus for minimal modal model generation

Cited in

(28)

• 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
• 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
• Efficient model generation through compilation.
• SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
• Paracoherent answer set computation
• Blocking and other enhancements for bottom-up model generation methods
• An incremental algorithm for generating all minimal models
• SHR tableaux -- a framework for automated model generation
• A tableau calculus for minimal modal model generation
• Exploring theories with a model-finding assistant
• scientific article; zbMATH DE number 1341481 (Why is no real title available?)
• scientific article; zbMATH DE number 1088032 (Why is no real title available?)
• Cautious reasoning in ASP via minimal models and unsatisfiable cores
• Minimal model generation with positive unit hyper-resolution tableaux
• A tableau calculus for minimal model reasoning
• Efficient model generation through compilation
• Constructing Bachmair-Ganzinger models
• First-order resolution methods for modal logics
• Better paracoherent answer sets with less resources
• ASP and subset minimality: enumeration, cautious reasoning and MUSes
• Range-restricted and Horn interpolation through clausal tableaux
• Some equalities are more equal than others
• A relevance restriction strategy for automated deduction
• Representing and building models for decidable subclasses of equational clausal logic
• Some techniques for proving termination of the hyperresolution calculus

Describes a project that uses

Uses Software

• SATCHMO
• FINDER

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)