Towards a Decidable LogicWeb via Length-Bounded Derivations

TL;DR

This paper introduces a length-bounded inference approach to LogicWeb, making it decidable and more manageable by limiting proof steps, and proposes a new module language for structuring logic programs and queries.

Contribution

It presents a novel length-bounded inference method for LogicWeb and a new module language for better program and query organization.

Findings

Length-bounded inference makes LogicWeb decidable.

The approach improves tractability of intractable queries.

A new module language enhances program structuring.

Abstract

LogicWeb has traditionally lacked devices for dealing with intractable queries. We address this limitation by adopting length-bounded inference, a form of approximate reasoning. A length-bounded inference is of the form $prov(P,G,n)$ which is a success if a query $G$ can be proved from the web page $P$ within $n$ proof steps. It thus makes LogicWeb decidable and more tractable. During the process, we propose a novel module language for logic programming as a device for structuring programs and queries.

Full text

{summary}

LogicWeb has traditionally lacked devices for dealing with intractable queries. We address this limitation by adopting length-bounded inference, a form of approximate reasoning. A length-bounded inference is of the form $pv({\cal P},G,n)$ which is a success if a query $G$ can be proved from the web page ${\cal P}$ within $n$ proof steps. It thus makes LogicWeb decidable and more tractable. During the process, we propose a novel module language for logic programming as a device for structuring programs and queries.

1 Introduction

Internet computing is an important modern programming paradigm. One successful attempt towards this direction is LogicWeb[4, 3]. LogicWeb is a model of the World Wide Web, where web pages are represented as logic programs, and hypertext links represents logical implications between these programs. Despite much attractiveness, LogicWeb (and its relatives such as Semantic Web[5]) has traditionally lacked elegant devices for dealing with intractable queries.

Dealing with intractable queries is a nontrivial task. Given the intractability of exact inference in large, distributed webs, it is essential to consider $approximate$ inference method. This paper proposes length-bounded inference which provides approximate inference. A length-bounded inference is of the form $pv({\cal P},G,n)$ which is a success if a query $G$ can be proved from a web page ${\cal P}$ within $n$ proof steps in a proof system such as the sequent calculus. Thus the accuracy of inference depends on $n$ and the user can choose the degree of accuracy of inference she wants by specifying a number $n$.

Although it might lose some completeness, there are several advantages with this approach.

• (1) 

It makes LogicWeb decidable and more tractable, while maintaining good expressibility.

• (2) 

In the real world, machines do not have unlimited resources and the notion of length-unbounded derivations is unrealistic. The notion of length-bounded derivations is a realistic, effective version of its counterpart.

• (3) 

Implementing our approach is quite easy and requires little overhead to the existing logic programming interpreter.

The notion of length-bounded derivations has been mainly used for analyzing the structures of proofs. To our knowledge, this is the first time that this notion is used for practical purposes.

Below we consider LogicWeb based on Horn clause logic with embedded implications. This logic extends Horn clauses by embedded implications of the form $D\supset G$ where $D$ is a Horn clause and $\supset$ is an implication. This has the following intended semantics: add $D$ to the program in the course of solving $G$. The remainder of this paper is structured as follows. We describe LWebB in the next section. In Section 4, we present some examples of LWebB. Section 5 concludes the paper.

2 Structuring Programs and Queries via Macros

Modern languages provide a module language as a device for structuring programs. We propose a novel device which is more flexible than traditional module languages. To be specific, our language provides a special macro function $/$ which binds a name to a clause or a query. This macro function serves to represent programs and queries in a concise way. For example, given two macro definitions $/p\ =\ father(tom,kim)$ and $/q\ =\ /p$, the notation $/p\land/q$ represents $father(tom,kim)\land father(tom,kim)$.

In contrast to traditional approaches, our module language has the following characteristics:

• •

Our macro languge can be used as a device for structuring queries. The difference between macro definition and predicate definition for structuring queries is that macros definitions are local and temporary. Macro definitions are thus not visible to clients.

• •

Our macro language is quite flexible, as modules (and queries) can be freely composed from submodules (and subqueries) via diverse logical connectives.

Macro definitions are typically processed before the execution but in our setting, it is possible to process macros and execute regular programs in an interleaved fashion. We adopt this approach below.

In this setting, we describe our language which is an extended version of Horn clauses with embedded implications. It is described by $G$-,$D$- and $M$-formulas given by the syntax rules below:

[TABLE]

In the rules above, $n$ is a name and $A$ represents an atomic formula. A $D$-formula is called a Horn clause with embedded implications. An $M$-formula is called macro definitions and ${\cal M}$ is a list of $M$-formulas.

Below, $G$-formulas will function as queries. A set of $D$-formulas and a list of $M$-formulas will constitute a program. We will present an operational semantics for this language. The rules of LWebB are formalized by means of what it means to execute a goal task $G$ from a program ${\cal P}$ with respect to ${\cal M}$. Below the notation $D;{\cal P}$ denotes $\{D\}\cup{\cal P}$ but with the $D$ formula being distinguished (marked for backchaining). Note that execution alternates between two phases: the goal-reduction phase (one without a distinguished clause) and the backchaining phase (one with a distinguished clause).

Definition 1**.**

Let $G$ be a goal, ${\cal P}$ be a program and ${\cal M}$ be a list macro definitions. Then the notion of executing $\langle{\cal P},G\rangle$ – $pv({\cal P},G)$ – is defined as follows:

• (1) 

$pv(A;{\cal P},A)$* % This is a success.*

• (2) 

$pv((G_{1}\supset A);{\cal P},A$* if $pv({\cal P},G_{1})$. % backchaining*

• (3) 

$pv(\forall xD;{\cal P},A)$* if $pv([t/x]D;{\cal P},A)$. % instantiation*

• (4) 

$pv(D_{1}\land D_{2};{\cal P},A)$* if $pv(D_{1};{\cal P},A)$. % use $D_{1}$ to solve $A$.*

• (5) 

$pv(D_{1}\land D_{2};{\cal P},A)$* if $pv(D_{2};{\cal P},A)$. % use $D_{2}$ to solve $A$.*

• (6) 

$pv(/n;{\cal P},A)$* if $pv(D;{\cal P},A)$ and $(/n=D)\in{\cal M}$. % we assume it chooses the most recent macro definition.*

• (7) 

$pv({\cal P},A)$* if $D\in{\cal P}$ and $pv(D;{\cal P},A)$. % change to backchaining phase.*

• (8) 

$pv({\cal P},G_{1}\land G_{2})$* if $pv({\cal P},G_{1})$ and $pv({\cal P},G_{2},)$. % conjunction*

• (9) 

$pv({\cal P},\exists xG_{1})$* if $pv({\cal P},[t/x]G_{1})$.*

• (10) 

$pv(\langle{\cal D},{\cal M}\rangle,D\supset G_{1})$* if $pv(\langle\{D\}\cup{\cal D},{\cal M}\rangle,G_{1})$ % an implication goal.*

• (11) 

$pv(\langle{\cal D},{\cal M}\rangle,/n:M\supset G_{1})$* if $pv(\langle\{/n\}\cup{\cal D},M::{\cal M}\rangle,G_{1})$ % an implication goal. Add new macros to the front of ${\cal M}$. Here $::$ is a list constructor.*

• (12) 

$pv({\cal P},/n)$* if $(/n=G)\in{\cal M}$ and $pv({\cal P},G)$. % a macroed query. We assume it chooses the most recent macro definition.*

3 Incorporating Bounded Derivations

We now incorporate the notion of bounded derivations into our previous language. This process is quite straightforward.

Definition 2**.**

Let $G$ be a goal, ${\cal P}$ be a program, ${\cal M}$ be macro definitions and $m$ be a number. Then the notion of executing $\langle{\cal P},G\rangle$ within $m$ steps and returning the proof length $n$ – $pv({\cal P},G,m,n)$ – is defined as follows:

• (1) 

$exec({\cal P},G,m)$* if $pv({\cal P},G,m,n)$. % call $pv$*

• (2) 

$pv(A;{\cal P},A,m,1)$* if $m>0$. % This is a success.*

• (3) 

$pv((G_{1}\supset A);{\cal P},A,m+1,n+1)$* if $pv({\cal P},G_{1},m,n)$. % backchaining*

• (4) 

$pv(\forall xD;{\cal P},A,m+1,n+1)$* if $pv([t/x]D;{\cal P},A,m,n)$. % instantiation*

• (5) 

$pv(D_{1}\land D_{2};{\cal P},A,m+1,n+1)$* if $pv(D_{1};{\cal P},A,m,n)$. % use $D_{1}$ to solve $A$.*

• (6) 

$pv(D_{1}\land D_{2};{\cal P},A,m+1,n+1)$* if $pv(D_{2};{\cal P},A,m,n)$. % use $D_{2}$ to solve $A$.*

• (7) 

$pv(/n;{\cal P},A,m+1,n+1)$* if $pv(D;{\cal P},A,m,n)$ and $(/n=D)\in{\cal M}$. % a macro definition*

• (8) 

$pv({\cal P},A,m+1,n+1)$* if $D\in{\cal P}$ and $pv(D;{\cal P},A,m,n)$. % change to backchaining phase.*

• (9) 

$pv({\cal P},G_{1}\land G_{2},m+1,n_{1}+n_{2}+1)$* if $pv({\cal P},G_{1},m,n_{1})$ and $pv({\cal P},G_{2},m-n_{1},n_{2})$. % proof length of $G_{i}$ is $n_{i}(i=1,2)$.*

• (10) 

$pv({\cal P},\exists xG_{1},m+1,n+1)$* if $pv({\cal P},[t/x]G_{1},m,n)$.*

• (11) 

$pv(\langle{\cal D},{\cal M}\rangle,D\supset G_{1},m+1,n+1)$* if $pv(\langle\{D\}\cup{\cal D},{\cal M}\rangle,G_{1},m,n)$ % an implication goal.*

• (12) 

$pv(\langle{\cal D},{\cal M}\rangle,/n:M\supset G_{1})$* if $pv(\langle\{/n\}\cup{\cal D},M::{\cal M}\rangle,G_{1})$ % an implication goal. Add new macros to the front of ${\cal M}$. Here $::$ is a list constructor.*

• (13) 

$pv({\cal P},/n,m+1,n+1)$* if $(/n=G)\in{\cal M}$ and $pv({\cal P},G,m,n)$. % a macroed query. We assume it chooses the most recent macro definition.*

In the above rules, choosing a term $t$ is a nontrivial task. Fortunately, this poses no problem as they can be obtained via the well-known unification process. The unification process delays the choices as much as possible until enough information is obtained. Note that the length of a derivation is based on the standard definition.

4 LWebB

In our context, a web page corresponds simply to a set of $M$-formulas within a file. An example of the use of this construct is provided by the following “lists” module which contains some basic list-handling rules and “arcs” module which contains some arcs between major cities.

[TABLE]

[TABLE]

These pages can be made available in specific contexts by explicitly mentioning the URL via a hyperlink.

It is well-known that some queries brings the machine into an infinite sequence of recursive calls. Such situations occur frequently in, for example, Prolog [1] with large programs. For example, consider a goal ?- $www.d.com/lists\supset www.d.com/arcs\supset path(london,boston)$. Solving this goal has the effect of adding the rules in $lists,arcs$ to the program before evaluating $path(london,boston)$. Note that this goal may not be terminating, depending on the implementation of the $path$ predicate.

To make this goal more tractable, we may want to use the length-bounded goal such as the one below:

?- (1000) $www.d.com/lists\supset www.d.com/arcs\supset path(london,boston)$. This goal obviously terminates, as it must be solved within 1000 proof steps.

5 Conclusion

In this paper, we have considered LWebB, a LogicWeb based on an extension to Prolog with embedded implications. This extension allows goals of the form $D\supset G$ where $D$ is a web page and $G$ is a goal.

LWebBalso adopts the length-bounded inference system in addition to the traditional inference system. This feature is particularly useful for making LogicWeb more tractable.

6 Acknowledgements

This work was supported by Dong-A University Research Fund.