Please use this identifier to cite or link to this item: http://hdl.handle.net/20.500.11889/4510
DC FieldValueLanguage
dc.contributor.authorYahya, Adnan-
dc.date.accessioned2017-03-14T07:34:27Z-
dc.date.available2017-03-14T07:34:27Z-
dc.date.issued2001-03-04-
dc.identifier.citationAdnan Yahya; Incorporating Bidirectional Relevancy into Model Generation Theorem Provers. Dagstuhl Seminar on Deduction. Dagstuhl, Germany. March 4-9, 2001en_US
dc.identifier.urihttp://hdl.handle.net/20.500.11889/4510-
dc.descriptionSeminar Convenors/Report Editors:Ulrich Furbach Universit at Koblenz-Landau Fachbereich Informatik Rheinau 1 56075 Koblenz Germany E-mail: uli@uni-koblenz.de Harald Ganzinger Max-Planck-Institut f ur Informatik Programming Logics Group Im Stadtwald D-66123 Saarbr ucken Germany E-mail: hg@mpi-sb.mpg.de Ryuzo Hasegawa Department of Electronics Kyushu University 36, Fukuoka 812, Japan E-mail: hasegawa@ele.kyuhsu-u.ac.jp Deepak Kapur University of New Mexico Dept. of Computer Science Farris Eng. Center # 339 NM87131 Albuquerque, USA E-mail: kapur@cs.unm.eduen_US
dc.description.abstractModel-generation theorem provers, SATCHMO-style, can explore a larger than needed search space when answering a query. Partial and total relevancy were suggested as a mechanisms to limit the search space to clauses that are needed for the refutation. SATCHMORE was an implementation of the latter. SATCHMORE relevancy, however, is driven by the entire set of negative clauses of the theory and no distinction is accorded to the query negation. Under unfavorable circumstances, such as in the presence of large amounts of negative data, this can reduce e ciency. In this lecture we de ne a further re nement of that uses only the negation of the query for relevancy determination at the start. Other negative clauses are introduced on demand and only if a refutation is not possible using the current set of negative clauses. The search for the relevant negative clauses is performed in a forward chaining mode as opposed to relevancy propagation in SATCHMORE which is based on backward chaining. The approach is shown to be refutationally sound and complete. Experiments on a prototype implementation point to its potential to enhance the effciency of the query answering process in disjunctive databases.en_US
dc.language.isoenen_US
dc.publisherSchloss Dagstuhl, Leibniz-Zentrum fuer Informatik; https://www.dagstuhl.de/en/en_US
dc.relation.ispartofseriesDagstuhl Report 300;300-
dc.subjectAutomatic theorem provingen_US
dc.subjectLogic, Symbolic and mathematicalen_US
dc.subjectArtificial intelligenceen_US
dc.titleIncorporating bidirectional relevancy into model generation theorem proversen_US
dc.typeConference Proceedingsen_US
newfileds.departmentEngineering and TechnologyEngineering and Technologyen_US
newfileds.conferenceDagstuhl Seminar on Deduction. Dagstuhl, Germany. March 4-9, 2001en_US
newfileds.item-access-typeopen_accessen_US
newfileds.thesis-prognoneen_US
newfileds.general-subjectComputers and Information Technology | الحاسوب وتكنولوجيا المعلوماتen_US
item.grantfulltextopen-
item.fulltextWith Fulltext-
item.languageiso639-1other-
Appears in Collections:Fulltext Publications
Files in This Item:
File Description SizeFormat
DagstuhlReport300Bidirectional01101-1.pdf156.38 kBAdobe PDFView/Open
Show simple item record

Page view(s)

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

Download(s)

9
checked on May 11, 2022

Google ScholarTM

Check


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