Negation and Proof by Contradiction in Access-Limited Logic

J. M. Crawford, B. J. Kuipers

Access-Limited Logic (ALL) is a language for knowledge representation which formalizes the access limitations inherent in a network structured knowledge-base. Where a deductive method such as resolution would retrieve all assertions that satisfy a given pattern, an access-limited logic retrieves all assertions reachable by following an available access path. In this paper, we extend previous work to include negation, disjunction, and the ability to make assumptions and reason by contradiction. We show that the extended ALLneg remains Socratically Complete (thus guaranteeing that for any fact which is a logical consequence of the knowledge-base, there exists a series of preliminary queries and assumptions after which a query of the fact will succeed) and computationally tractable. We show further that the key factor determining the computational difficulty of finding such a series of preliminary queries and assumptions is the depth of assumption nesting. We thus demonstrate the existence of a family of increasingly powerful inference methods, parameterized by the depth of assumption nesting, ranging from incomplete and tractable to complete and intractable.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.