Please use this identifier to cite or link to this item: http://hdl.handle.net/20.500.11889/4454
DC FieldValueLanguage
dc.contributor.authorYahya, Adnan
dc.contributor.authorPlaisted, David A.
dc.date.accessioned2017-03-09T09:48:02Z
dc.date.available2017-03-09T09:48:02Z
dc.date.issued2002-03-01
dc.identifier.urihttp://hdl.handle.net/20.500.11889/4454
dc.description.abstractA family of tableau methods, called ordered semantic hyper (OSH) tableau methods for first-order theories with function symbols, is presented. These methods permit semantic information to guide the search for a proof. They also may make use of orderings on literals, clauses, and interpretations to guide the search. In a typical tableau, the branches represent conjunctions of literals, and the tableau represents the disjunction of the branches. An OSH tableau is as usual except that each branch B has an interpretation I0[B] associated with it, where I0 is an interpretation supplied at the beginning and I0[B] is the interpretation most like I0 that satisfies B. Only clauses that I0[B] falsifies may be used to expand the branch B, thus restricting the kinds of tableau that can be constructed. This restriction guarantees the goal sensitivity of these methods if I0 is properly chosen. Certain choices of I0 may produce a purely bottom-up tableau construction, while others may result in goal-oriented evaluation for a given query. The choices of which branch is selected for expansion and which clause is used to expand this branch are examined and their effects on the OSH tableau methods considered. A branch reordering method is also studied, as well as a branch pruning technique called complement modification, that adds additional literals to branches in a soundness-preserving manner. All members of the family of OSH tableaux are shown to be sound, complete, and proof convergent for refutations. Proof convergence means that any allowable sequence of operations will eventually find a proof, if one exists. OSH tableaux are powerful enough to be treated as a generalization of several classes of tableau discussed in the literature, including forward chaining and backward chaining procedures. Therefore, they can be used for efficient query processing.en_US
dc.language.isoen_USen_US
dc.publisherSpringer Verlagen_US
dc.relation.ispartofseriesdoi:10.1023/A:1020512924736;
dc.subjecttableaux semanticsen_US
dc.subjectAutomatic theorem provingen_US
dc.subjectliteral orderingen_US
dc.subjectArtificial intelligenceen_US
dc.titleOrdered semantic hypertableauxen_US
dc.typeArticleen_US
newfileds.departmentEngineering and TechnologyEngineering and Technologyen_US
newfileds.conferenceJournal of Automated Reasoning:29(1):17-57 (2002)en_US
newfileds.item-access-typebzuen_US
newfileds.thesis-prognoneen_US
newfileds.general-subjectBiotechnology and Genetic Engineering | التكنولوجيا الحيوية والهندسة الوراثيةen_US
item.grantfulltextopen-
item.fulltextWith Fulltext-
item.languageiso639-1other-
Appears in Collections:Fulltext Publications
Files in This Item:
File Description SizeFormat
OrderedSemanticHyperTableauxAbstract.pdf83.87 kBAdobe PDFView/Open
Show simple item record

Page view(s)

58
Last Week
0
Last month
2
checked on May 11, 2022

Download(s)

5
checked on May 11, 2022

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.