Please use this identifier to cite or link to this item: http://hdl.handle.net/20.500.11889/4510
Title: Incorporating bidirectional relevancy into model generation theorem provers
Authors: Yahya, Adnan
Keywords: Automatic theorem proving
Logic, Symbolic and mathematical
Artificial intelligence
Issue Date: 4-Mar-2001
Publisher: Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik; https://www.dagstuhl.de/en/
Citation: Adnan Yahya; Incorporating Bidirectional Relevancy into Model Generation Theorem Provers. Dagstuhl Seminar on Deduction. Dagstuhl, Germany. March 4-9, 2001
Series/Report no.: Dagstuhl Report 300;300
Abstract: Model-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.
Description: Seminar 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.edu
URI: http://hdl.handle.net/20.500.11889/4510
Appears in Collections:Fulltext Publications

Files in This Item:
File Description SizeFormat 
DagstuhlReport300Bidirectional01101-1.pdf156.38 kBAdobe PDFView/Open


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