On deciding subsumption problems

DOI10.1007/S10472-005-0434-4MaRDI QIDQ1777407zbMATH OpenOpenAlexFDO

Authors Uwe Egly, Reinhard Pichler, Stefan Woltran

Publication date 13 May 2005

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-005-0434-4

zbMATH Keywords

satisfiabilitysubsumptionQBFsequational problems

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• scientific article; zbMATH DE number 1342223
• Generalized subsumption and its applications to induction and redundancy
• Logic for Programming, Artificial Intelligence, and Reasoning
• scientific article; zbMATH DE number 970722
• Subsumption algorithms based on search trees

Cites work

• scientific article; zbMATH DE number 1615238 (Why is no real title available?)
• scientific article; zbMATH DE number 3904558 (Why is no real title available?)
• scientific article; zbMATH DE number 4053011 (Why is no real title available?)
• scientific article; zbMATH DE number 176121 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1305704 (Why is no real title available?)
• scientific article; zbMATH DE number 1342223 (Why is no real title available?)
• scientific article; zbMATH DE number 549974 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1950260 (Why is no real title available?)
• scientific article; zbMATH DE number 1507193 (Why is no real title available?)
• scientific article; zbMATH DE number 1765680 (Why is no real title available?)
• scientific article; zbMATH DE number 2085248 (Why is no real title available?)
• scientific article; zbMATH DE number 1844493 (Why is no real title available?)
• A non-ground realization of the stable and well-founded semantics
• A structure-preserving clause form translation
• An Efficient Unification Algorithm
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• BerkMin: A fast and robust SAT-solver
• Equational formulae with membership constraints
• Equational problems and disunification
• Explicit representation of terms defined by counter examples
• Hyperresolution and automated model building
• Resolution for quantified Boolean formulas
• SATO: An efficient propositional prover
• Sufficient-completeness, ground-reducibility and their complexity
• The polynomial-time hierarchy
• Working with ARMs: Complexity results on atomic representations of Herbrand models

Cited in

(2)

• A problem in the theory of subordination
• On anti-subsumptive knowledge enforcement

Describes a project that uses

Uses Software

• semprop
• QUBE
• BerkMin
• Chaff
• SATO
• QuBE++

This page was built for publication: On deciding subsumption problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1777407)