Date Available

12-7-2011

Year of Publication

2003

Document Type

Thesis

College

Engineering

Department

Computer Science

First Advisor

Judy Goldsmith

Abstract

Boolean formulas can be used to model real-world facts. In some situation we may havea Boolean formula that closely approximates a real-world fact, but we need to fine-tune itso that it models the real-world fact exactly. This is a problem of theory revision where thetheory is in the form of a Boolean formula. An algorithm is presented for revising a class ofBoolean formulas that are expressible as conjunctions of Horn clauses. Each of the clausesin the formulas considered here has a unique unnegated variable that does not appear inany other clauses, and is not `F'. The revision algorithm uses equivalence and membershipqueries to revise a given formula into a formula that is equivalent to an unknown targetformula having the same set of unnegated variables. The amount of time required by thealgorithm to perform this revision is logarithmic in the number of variables, and polynomialin the number of clauses in the unknown formula. An early version of this work waspresented at the 2003 Midwest Artificial Intelligence and Cognitive Science Conference [4].

Download

Share

COinS