Title :
Uniform proofs and disjunctive logic programming
Author :
Nadathur, Gopalan ; Loveland, Donald W.
Author_Institution :
Dept. of Comput. Sci., Chicago Univ., IL, USA
Abstract :
One formulation of the concept of logic programming is the notion of an abstract logic programming language. Central to its definition is a uniform proof, which enforces the requirements of inference direction, including goal-directedness, and the duality of readings, both declarative and procedural. We use this technology to investigate disjunctive logic programming (DLP), an extension of traditional logic programming that permits disjunctive program clauses. This extension has been considered by some to be inappropriately identified with logic programming because the indefinite reasoning introduced by disjunction violates the goal-oriented search directionality that is central to logic programming. We overcome this criticism by showing that the requirement of uniform provability can be realized in a logic which is more general than that of DLP under a modest, sound modification of programs. We use this observation to derive inference rules that capture the essential proof structure of InH-Prolog (Inheritance Near-Horn Prolog), a known proof procedure for DLP
Keywords :
duality (mathematics); formal languages; inference mechanisms; logic programming; logic programming languages; programming theory; search problems; theorem proving; InH-Prolog; Inheritance Near-Horn Prolog; abstract logic programming language; declarative programming; disjunctive logic programming; disjunctive program clauses; duality of readings; goal-directedness; goal-oriented search directionality; indefinite reasoning; inference direction; inference rules; procedural programming; proof structure; sound program modification; uniform proofs; uniform provability; Books; Calculus; Computer science; Databases; Logic programming;
Conference_Titel :
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7050-9
DOI :
10.1109/LICS.1995.523252