In this paper, a pushdown automaton, with an infinite set of states as a partially ordered set (poset), is formulated, and its control problem of whether a given configuration can be transferred to another is discussed. For the controllability to be decidable, we take a condition the poset satisfies, that is, a condition that there are only finite number of states under the partial ordering between two given states. The control problem is decidable in polynomial time on condition the length of each pushed stack string is bounded by a constant in a given pushdown automaton. The motivation of considering the control problem comes up from the stack structure in implementing the SLD resolution deductions, in which the leftmost atom in each goal is selected and unified with some procedure name (that is, some head) of a definite clause, with the effect of the procedure name being replaced by the procedure bodies and unifications. Thus, the control problem is applied to describe the SLD resolution deductions of finite steps, by constructing a pushdown automaton model for a set of definite clauses, in which leftmost selection of atom in each goal forms a stack structure and substitutions affecting goals are interpreted as states. When constructing a pushdown automaton model for an SLD resolution deduction, algebraic properties of the idempotent substitution set, which are used in unifications, are examined and utilized. The quotient set of the idempotent substitution set per renamings is adopted to present the automaton model.

We deal with a fixpoint semantics for normal logic programs by means of an algebraic manipulation of idempotent substitution sets. Because of the negation, the function associated with a given normal logic program, which captures the deductions caused by the program, is in general nonmonotonic, as long as we are concerned with 2-valued logic approach. The demerit of the nonmonotonic function is not to guarantee its fixpoint well, although the fixpoint is regarded as representing the whole behaviour. The stable model as in [6] is fixpoint of nonmonotonic functions, but it is referred to on the assumption of its existences. On the other hand, if we take 3-valued logic approach for normal logic programs as in [5], [9], [11], [14] we have the monotonic function to represent resolutions and negation as failure, and define its fixpoint well, if we permit the fixpoint not to be constructive because of discontinuity. Since the substituitions for variables in the program are essentially significant in the deductions for logic programming, we next focus on the representations by means of substitutions for the deductions, without usual expressions based on atomic formulas. We examine the semantics in terms of abstract interpretations among semantics as surveyed in [9], where an abstraction stands for the capability of representing another semantics. In this paper, in 3-valued logic approach and by means of the substitution manipulation, the semantics is defined to be an abstraction of the semantics in [5], [9]. To construct a semantics based on the idempotent substitution set, the algebraic manipulation of substitutions is significant, whereas the treatment in [10] for the case of definite clause sets is not available because of the restriction of substitutions to some variable domain as most general unifications.

In this paper we give a method of transforming logic programs into equational dataflow programs. The equational dataflow program is a set of recursion equations as to variables over a sequence domain. A recursion equation corresponds to each definite (Horn) clause which is interpreted as a transformation of variables to a variable. Each variable denotes a function from the set of natural numbers to the Herbrand base, that is, a sequence of ground atoms. The fair merge function is necessary to realize OR-nondeterminism, which is essential in the deductions of logic programs, by means of an equational dataflow program. The nondeterminism in the transformation caused by a definite clause is eliminated and ensured fair by introducing a kind of oracle which will also be provided by simple recursion equations. Then it will be shown that the equational dataflow program with the oracle is both sound and complete in denoting the finite computation of the original logic program. The semantics of the equational dataflow program is given by fixpoint approach and is interpreted as a semantics of the given logic program.

In this paper, a network of communicating logic programs is proposed as a model for concurrent programming based on logic programs with explicit channels of communications. On the assumption that the denotations of channels are defined by using a sequence domain, semantics for unbounded nondeterminism caused by logic programs is dealt with and the whole network is defined as an extension of Kahn's pure dataflow. A denotational semantics for the whole network is defined by a recursive relation set as to the histories of channels. The method to investigate extensionality of input-output histories on the node in nondeterministic dataflow is not applicable to the proposed network, because the node is a logic program. Fairness is required for unbounded nondeterminism to describe the behaviour of the whole network. And in this paper the corresponding semantics of the network is shown. We have a method of defining a continuous function which is associated with the network, based on histories of channels. The least fixpoint of the function is regarded as a denotational semantics for the whole network, to reflect its fair behaviours.

There have been semantics for logic programs as sets of definite clauses over sequence domains in [2],[6]. The sequence of substitutions caused by resolutions for logic programs can be captured by a fixpoint of a functional [3],[16]. In [15], a functional is regarded as a behaviour of a dataflow network, the semantics over sequence domains induces dataflow computing for logic programs. Also it may provide a transformation of logic programs to functional programs[16]. Motivated by dataflow computing constructions for logic programming, this paper deals with fixpoint semantics over sequence domains for logic programs with equations and negations. A transformation, representing deductions caused by resolutions and narrowings, is associated with a logic program with equations, modified from the operator in [18], so that it may be represented by a continuous functional over a sequence domain, and its least fixpoint is well-defined. An explicit construction of such a continuous functional of sequence variables is necessary for dataflow computing, and we should prove that the functional of sequence variables can exactly represent the transformation concerned with sets. For a general logic program, a functional is constructed over a sequence domain so that it may reflect a consistency-preserving renewal function for the pair of atom sets on the basis of the 3-valued logic approach as in [7], and [11]. It is a problem to construct the domain for the functional representing a generation of atom sets interpreted as true and negation as failure in the generation, for general logic programs. The functional is monotonic over a complete partial order and its least fixpoint is well-defined, although the least fixpoint is not always obtained by the limit of finite computing, because of the functional being not necessarily continuous.

We are concerned with semantic views on an extended version of SLD resolution with negation as failure (SLDNF resolution) for normal logic programs, which Eshghi and Kowalski (1989) presented by making the SLDNF resolution capable of keeping negated predicates in memory and of extracting abducible predicates. This paper deals with its formal representation in relational form, for the purpose of interpreting the normal goal as an acquisitor of negated predicates stored in memory. Some set acquired by the derivations which the normal goal evokes is defined to be a semantics of the goal, under the constraint that the set is as large as possible and does not violate consistency in model theory. The semantics is discussed with relation to the 3-valued logic model theory, where the model theory is represented by alternating fixpoint semantics (Van Gelder, 1993). For simplicity of treatment, this paper is concerned with the normal logic program in the propositional logic.

This paper deals with distributed procedures, caused by negation as failure through a network, where general logic programs are distributed so that they communicate with each other in terms of negation as failure inquiries and responses, but not in terms of derivations of SLD resolutions. The common variables as channels in share for distributed programs are not treated, but negation as failure validated in the whole network is the object for communications of distributed programs. We can define the semantics for the distributed programs in a network. At the same time, we have distributed proof procedures for distributed programs, by means of negation as failure to be implemented through the network, where the soundness of the procedure is guaranteed by the defined semantics.

The Horn set is the set of Horn clauses. The Horn clause is the set of literals which contains at most one positive literal, where a positive literal means a literal without negation sign. The satisfiability problem of the Horn set in propositional logic is one of P-complete problems, although the satisfiability problem of the formula in propositional logic is one of typical NP-complete problems. In propositional logic, unit and input resolutions, proposed by C. L. Chang, are complete inference rules used to detect the satisfiability of the Horn set. In this paper, we formulate a Restricted Linear (RL) deduction, extending unit and input resolutions. The RL deduction is formed by layering linear deductions each of which corresponds to an input resolution refutation, and is called by another name, a Linear Layered Resolution deduction based on Input resolution (an LLRI deduction). Next, we formulate a Nonlinear Layered Resolution deduction based on Input resolutions (an NLRI deduction). By means of the LLRI and NLRI deductions, we propose some classes of extended Horn sets in propositional logic for which the satisfiability problems are solvable by LLRI and NLRI deductions in deterministic polynomial time; and, thus, so are P-complete. Also we propose algorithms to determine whether a given set of clauses is in the proposed classes of extended Horn sets.

Negation as failure is realized to be combined with SLD resolution for general logic programs, where the combined resolution is called an SLDNF resolution. In this paper, we introduce narrowing and infinite failure to SLDNF resolution for general logic programs with equations. The combination of SLDNF resolution with narrowing and infinite failure is called an SLDNFN resolution. In Shepherdson (1992), equation theory is combined with SLDNF resolution so that the soundness may be guaranteed with respect to Clark's completion. Generalizing the method of Yamamoto (1987) for definite clause sets with equations, we formally define a least fixpoint semantics, which is an extension of Fitting (1985) and Kunen (1987) semantics, and which includes the pair of success and failure sets defined by the SLDNFN resolution. The relationship between the fixpoint semantics and the pair of sets is regarded as an extension of the relationships for general logic programs as in Marriott and et al. (1992) and in Yamasaki (1996). Instead of generalizing Clark's completion for SLDNFN resolution, we establish, as a model for general logic programs with equations, an extended well-founded model so that the SLDNFN resolution is sound and complete for non-floundering queries with respect to the extended well-founded model.