Semantically-Guided Goal-Sensitive Reasoning: Model Representation

SGGS (Semantically-Guided Goal-Sensitive reasoning) is a clausal theorem-proving method, which generalizes to first-order logic the Davis-Putnam-Loveland-Logemann procedure with conflict-driven clause learning (DPLL-CDCL). SGGS starts from an initial interpretation, and works towards modifying it into a model of a given set of clauses, reporting unsatisfiability if there is no model. The state of the search for a model is described by a structure, called SGGS clause sequence. We present SGGS clause sequences as a formalism to represent models; and we prove their properties related to the mechanisms of SGGS for clausal propagation, conflict solving, and conflict-driven model repair at the first-order level.     

Totally correct logic program transformations via well-founded annotations

We address the problem of proving the total correctness of transformations of definite logic programs. We consider a general transformation rule, called clause replacement, which consists in transforming a program P into a new program Q by replacing a set Γ ₁ of clauses occurring in P by a new set Γ ₂ of clauses, provided that Γ ₁ and Γ ₂ are equivalent in the least Herbrand model M(P) of the program P. We propose a general method for proving that transformations based on clause replacement are totally correct, that is, M(P)=M(Q). Our method consists in showing that the transformation of P into Q can be performed by: (i) adding extra arguments to predicates, thereby deriving from the given program P an annotated program $\overline{P}$ , (ii) applying a variant of the clause replacement rule and transforming the annotated program $\overline{P}$ into a terminating annotated program $\overline{Q}$ , and (iii) erasing the annotations from $\overline{Q}$ , thereby getting Q. Our method does not require that either P or Q are terminating and it is parametric with respect to the annotations. By providing different annotations we can easily prove the total correctness of program transformations based on various versions of the popular unfolding, folding, and goal replacement rules, which can all be viewed as particular cases of our clause replacement rule.     

Hardness results for approximate pure Horn CNF formulae minimization

We study the hardness of approximation of clause minimum and literal minimum representations of pure Horn functions in n Boolean variables. We show that unless P=NP, it is not possible to approximate in polynomial time the minimum number of clauses and the minimum number of literals of pure Horn CNF representations to within a factor of \(2^{\log^{1-o(1)} n}\) . This is the case even when the inputs are restricted to pure Horn 3-CNFs with O(n ^1+ε ) clauses, for some small positive constant ε. Furthermore, we show that even allowing sub-exponential time computation, it is still not possible to obtain constant factor approximations for such problems unless the Exponential Time Hypothesis turns out to be false.     

On deciding subsumption problems

Subsumption is an important redundancy elimination method in automated deduction. A clause D is subsumed by a set C of clauses if there is a clause CC and a substitution such that the literals of C are included in D. In the field of automated model building, subsumption has been modified to an even stronger redundancy elimination method, namely the so-called clausal H-subsumption. Atomic H-subsumption emerges from clausal H-subsumption by restricting D to an atom and C to a set of atoms. Both clausal and atomic H-subsumption play an indispensable key role in automated model building. Moreover, problems equivalent to atomic H-subsumption have been studied with different terminologies in many areas of computer science. Both clausal and atomic H-subsumption are known to be intractable, i.e., ₂ ^p -complete and NP-complete, respectively. In this paper, we present a new approach to deciding (clausal and atomic) H-subsumption that is based on a reduction to QSAT₂ and SAT, respectively.     

The Prolog not-predicate and negation as failure rule

Clark’s query evaluation procedure for computing negative information in deductive databases using a “negation as failure” inference rule requires a safe computation rule which may only select negative literals if they are ground. This is a very restrictive condition, which weakens the usefulness of negation as failure in a query evaluation procedure. This paper studies the definition and properties of the “not” predicate defined in most Prolog systems which do not enforce the above mentioned condition of a safe computation rule. We show that the negation in clauses and the “not” Predicate of Prolog are not the same. In fact a Prolog program may not be in clause form. An extended query evaluation procedure with an extended safe computation rule is proposed to evaluate queries which involve the “not” predicate. The soundness and completeness of this extended query evaluation procedure with respect to a class of logic programs are proved. The implementation of such an extended query evaluation procedure in a Prolog system can be implemented by a preprocessor for executing range restricted programs and requires no modification to the interpreter/compiler of an existing Prolog system. We compare this proposed extended query evaluation procedure with the extended program proposed by Lloyd and Topor, and the negation constructs in NU-Prolog. The use of the “not” predicate for integrity constraint checking in deductive databases is also presented.     

P-Prolog: A parallel logic language based on exclusive relation

This paper presents a parallel logic programming language named P-Prolog which is being developed as a logic programming language featuring both and- and or-parallelism. Compared with the other parallel logic programming languages, syntactic constructs such as read-only annotation,⁶⁾ mode declaration²⁾ and communication constraints⁷⁾ are not used in P-Prolog. A new concept introduced in P-Prolog is the exclusive relation of guarded Horn clauses. Advances included in P-prolog. are:

1. The synchronization mechanism can determine the direction of data flow dynamically.
2. Guarded Horn clauses can be interpreted as eitherdon’t care nondeterminism ordon’t know non-determinism.

A prototype interpreter of P-Prolog has been implemented in C-Prolog. We are now implementing a P-Prolog interpreter in the C language.     

Inductive inference of monotonic formal systems from positive data

A formal system is a finite set of expressions, such as a grammar or a Prolog program. A semantic mapping from formal systems to concepts is said to be monotonic if it maps larger formal systems to larger concepts. A formal system Γ is said to be reduced with respect to a finite setX if the concept defined by Γ containsX but the concepts defined by any proper subset Γ′ of Γ cannot contain some part ofX. Assume a semantic mapping is monotonic and formal systems consisting of at mostn expressions that are reduced with respect toX can define only finitely many concepts for any finite setX and anyn. Then, the class of concepts defined by formal systems consisting of at mostn expressions is shown to be inferable from positive data. As corollaries, the class of languages defined by length-bounded elementary formal systems consisting of at most,n axioms, the class of languages generated by context-sensitive grammars consisting of at mostn productions, and the class of minimal models of linear Prolog programs consisting of at mostn definite clauses are all shown to be inferable from positive data.     

A logic programming language based on the Andorra model

The Andorra model is a parallel execution model of logic programs which exploits the dependent and-parallelism and or-parallelism inherent in logic programming. We present a flat subset of a language based on the Andorra model, henceforth called Andorra Prolog, that is intended to subsume both Prolog and the committed choice languages. Flat Andorra, in addition todon’t know anddon’t care nondeterminism, supports control of or-parallel split, synchronisation on variables, and selection of clauses. We show the operational semantics of the language, and its applicability in the domain of committed choice languages. As an examples of the expressiveness of the language, we describe a method for communication between objects by time-stamped messages, which is suitable for expressing distributed discrete event simulation applications. This method depends critically on the ability to expressdon’t know nondeterminism and thus cannot easily be expressed in a committed choice language.     

A New Lower Bound on the Maximum Number of Satisfied Clauses in Max-SAT and Its Algorithmic Applications

A pair of unit clauses is called conflicting if it is of the form (x), $(\bar{x})$ . A CNF formula is unit-conflict free (UCF) if it contains no pair of conflicting unit clauses. Lieberherr and Specker (J. ACM 28:411?C421, 1981) showed that for each UCF CNF formula with m clauses we can simultaneously satisfy at least $\hat{ \varphi } m$ clauses, where $\hat{ \varphi }=(\sqrt{5}-1)/2$ . We improve the Lieberherr-Specker bound by showing that for each UCF CNF formula F with m clauses we can find, in polynomial time, a?subformula F?? with m?? clauses such that we can simultaneously satisfy at least $\hat{ \varphi } m+(1-\hat{ \varphi })m'+(2-3\hat {\varphi })n''/2$ clauses (in F), where n?? is the number of variables in F which are not in F??. We consider two parameterized versions of MAX-SAT, where the parameter is the number of satisfied clauses above the bounds m/2 and $m(\sqrt{5}-1)/2$ . The former bound is tight for general formulas, and the later is tight for UCF formulas. Mahajan and Raman (J. Algorithms 31:335?C354, 1999) showed that every instance of the first parameterized problem can be transformed, in polynomial time, into an equivalent one with at most 6k+3 variables and 10k clauses. We improve this to 4k variables and $(2\sqrt{5}+4)k$ clauses. Mahajan and Raman conjectured that the second parameterized problem is fixed-parameter tractable (FPT). We show that the problem is indeed FPT by describing a polynomial-time algorithm that transforms any problem instance into an equivalent one with at most $(7+3\sqrt{5})k$ variables. Our results are obtained using our improvement of the Lieberherr-Specker bound above.     

Design and simulation of a sequential Prolog machine

Prolog-X is an implemented portable interactive sequential Prolog system in which clauses are incrementally compiled for a virtual machine called the ZIP Machine. At present, the ZIP Machine is emulated by software, but it has been designed to permit easy implementation in microcode or hardware. Prolog-X running on the software-based emulator provides performance comparable with existing Prolog interpreters. To demonstrate its efficiency, compatibility, and comprehensiveness of implementation, Prolog-X has been used to compile and run several large applications programs. Several novel techniques are used in the implementation, particularly in the areas of the representation of therecordx database, the selection of clauses, and the compilation of arithmetic expressions.     

Complexity of Clausal Constraints Over Chains

We investigate the complexity of the satisfiability problem of constraints over finite totally ordered domains. In our context, a clausal constraint is a disjunction of inequalities of the form x≥d and x≤d. We classify the complexity of constraints based on clausal patterns. A pattern abstracts away from variables and contains only information about the domain elements and the type of inequalities occurring in a constraint. Every finite set of patterns gives rise to a (clausal) constraint satisfaction problem in which all constraints in instances must have an allowed pattern. We prove that every such problem is either polynomially decidable or NP-complete, and give a polynomial-time algorithm for recognizing the tractable cases. Some of these tractable cases are new and have not been previously identified in the literature.     

From software extensions to product lines of dataflow programs

Dataflow programs are widely used. Each program is a directed graph where nodes are computations and edges indicate the flow of data. In prior work, we reverse-engineered legacy dataflow programs by deriving their optimized implementations from a simple specification graph using graph transformations called refinements and optimizations. In MDE speak, our derivations were PIM-to-PSM mappings. In this paper, we show how extensions complement refinements, optimizations, and PIM-to-PSM derivations to make the process of reverse engineering complex legacy dataflow programs tractable. We explain how optional functionality in transformations can be encoded, thereby enabling us to encode product lines of transformations as well as product lines of dataflow programs. We describe the implementation of extensions in the \(\mathtt{ReFlO}\) tool and present two non-trivial case studies as evidence of our work’s generality.     

On deciding subsumption problems

Subsumption is an important redundancy elimination method in automated deduction. A clause D is subsumed by a set of clauses if there is a clause C and a substitution such that the literals of C are included in D. In the field of automated model building, subsumption has been modified to an even stronger redundancy elimination method, namely the so-called clausal H-subsumption. Atomic H-subsumption emerges from clausal H-subsumption by restricting D to an atom and to a set of atoms. Both clausal and atomic H-subsumption play an indispensable key role in automated model building. Moreover, problems equivalent to atomic H-subsumption have been studied with different terminologies in many areas of computer science. Both clausal and atomic H-subsumption are known to be intractable, i.e., _p ² -complete and NP-complete, respectively. In this paper, we present a new approach to deciding (clausal and atomic) H-subsumption that is based on a reduction to QSAT₂ and SAT, respectively.This was partially supported by the Austrian Science Foundation under grant P15068. We thank the anonymous referees for valuable comments.     

Extremal problems in logic programming and stable model computation

We study the following problem: given a class of logic programs ¢, determine the maximum number of stable models of a program from ©. We establish the maximum for the class of all logic programs with at most n clauses, and for the class of all logic programs of size at most n. We also characterize the programs for which the maxima are attained. We obtained similar results for the class of all disjunctive logic programs with at most n clauses, each of length at most m, and for the class of all disjunctive logic programs of size at most n. Our results on logic programs have direct implication for the design of algorithms to compute stable models. Several such algorithms, similar in spirit to the Davis-Putnam procedure, are described in the paper. Our results imply that there is an algorithm that finds all stable models of a program with n clauses after considering the search space of size O(3^n/3) in the worst case. Our results also provide some insights into the question of representability of families of sets as families of stable models of logic programs.     

On finding short resolution refutations and small unsatisfiable subsets

We consider the parameterized problems of whether a given set of clauses can be refuted within k resolution steps, and whether a given set of clauses contains an unsatisfiable subset of size at most k  . We show that both problems are complete for the class W[1]$\mathrm{W}[1]$, the first level of the W-hierarchy of fixed-parameter intractable problems. Our results remain true if restricted to 3-SAT instances and/or to various restricted versions of resolution including tree-like resolution, input resolution, and read-once resolution. Applying a metatheorem of Frick and Grohe, we show that, restricted to classes of sets of clauses of locally bounded treewidth, the considered problems are fixed-parameter tractable. For example, the problems are fixed-parameter tractable for planar CNF formulas.     

Bounded-wait merge in Shapiro’s Concurrent Prolog

InA Subset of Concurrent Prolog and Its Interpreter (1983), E. Y. Shapiro introduces the language Concurrent Prolog. In his presentation, the problem of guaranteeing bounded-waiting during a merge operation is used as a programming example. Solutions are proposed for binary and n-ary merges. The solutions are, however, completely dependent on specific operational characteristics of a Concurrent Prolog machine or interpreter. This paper presents an alternate approach in which the property of bounded-waiting is incorporated into the semantics of the programs, demonstrable given only the computational model of the language. The solution strategy is to utilize the familiar systems programming techniques of block-on-input and busy-wait. This approach requires that the language be augmented with a metalogical predicate analogous to thevar(_) predicate of Sequential Prolog. The resultant programs are interesting and illustrative examples of Concurrent Prolog as a programming language.     

Specification and initialization of a logic computer system

A logic computer system consists of an inference machine and a compatible logic operating system. This paper describes prospective models for a logic computer system, and its hardware and software components. The language Concurrent Prolog serves as the single implementation, specification, and machine language. The computer system is represented as a logic programming goallogic_computer_system. Specification of the system corresponds to resolution of this goal. Clauses used to solve the goal — and ensuing subgoals — progressively refine the machine, operating system, and computer system designs. In addition, the accumulation of all clauses describing the logic operating system constitute its implementation. Logic computer systems with vastly different fundamental characteristics can be concisely specified in this manner. Two contrasting examples are given and discussed. An important characteristic of both peripheral devices and the overall computer system, whether they are restartable or perpetual, is examined. As well, a method for operational initialization of the logic computer system is presented. The same clauses which incrementally specify characteristics of the computer system also describe the manner in which this initialization takes place.     

Rewrite-Based Decision Procedures

The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that an inference system generates finitely many clauses from the presentation of a theory and a finite set of ground unit clauses, then any fair strategy based on that system can be used as a -satisfiability procedure. In this paper, we introduce a set of sufficient conditions to generalize the entire framework of rewrite-based -satisfiability procedures to rewrite-based -decision procedures. These conditions, collectively termed subterm-inactivity, will allow us to obtain rewrite-based -decision procedures for several theories, namely those of equality with uninterpreted functions, arrays with or without extensionality and two of its extensions, finite sets with extensionality and recursive data structures.     

Parallel complexity of logical query programs

We consider the parallel time complexity of logic programs without function symbols, called logical query programs, or Datalog programs. We give a PRAM algorithm for computing the minimum model of a logical query program, and show that for programs with the “polynomial fringe property,” this algorithm runs in time that is logarithmic in the input size, assuming that concurrent writes are allowed if they are consistent. As a result, the “linear” and “piecewise linear” classes of logic programs are inN C. Then we examine several nonlinear classes in which the program has a single recursive rule that is an “elementary chain.” We show that certain nonlinear programs are related to GSM mappings of a balanced parentheses language, and that this relationship implies the “polynomial fringe property;” hence such programs are inN C Finally, we describe an approach for demonstrating that certain logical query programs are log space complete forP, and apply it to both elementary single rule programs and nonelementary programs.