Positive unit hyperresolution tableaux and their application to minimal model generation

DOI10.1023/A:1006291616338zbMath0960.03006OpenAlexW2150903551MaRDI QIDQ1581852

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

Herbrand modelsproof theorytableaumodel generationminimal modelfirst-order clauses

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (18)

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

• FINDER
• SATCHMO

This page was built for publication: Positive unit hyperresolution tableaux and their application to minimal model generation