Experiments with semantic paramodulation

A semantic restriction is presented for use with paramodulation in automated theorem-proving programs. The method applies to first-order formulas with equality whole clause forms are Horn sets. In this method, an interpretation is given to the program along with the set of clauses to be refuted. The intention is to have the interpretation serve as an example to guide the search for a refutation. The semantic restriction was incorporated into an existing automated theorem-proving program, and a number of experiments were conducted on theorems in abstract algebra. Semantic paramodulation is an extension of set-of-support paramodulation. A comparison of the two strategies was used as the basis for experimentation. The semantic searches performed markedly better than the corresponding set-of-support searches in many of the comparisons. The semantic restriction seems to make the program less sensitive to the choice of rewrite rules and supported clauses.     

On renamable Horn and generalized Horn functions

A Boolean function in disjunctive normal form (DNF) is aHorn function if each of its elementary conjunctions involves at most one complemented variable. Ageneralized Horn function is constructed from a Horn function by disjuncting a nested set of complemented variables to it. The satisfiability problem is solvable in polynomial time for both Horn and generalized Horn functions. A Boolean function in DNF is said to berenamable Horn if it is Horn after complementation of some variables. Succinct mathematical characterizations and linear-time algorithms for recognizing renamable Horn and generalized Horn functions are given in this paper. The algorithm for recognizing renamable Horn functions gives a new method to test 2-SAT. Some computational results are also given.The authors were supported in part by the Office of Naval Research under University Research Initiative grant number N00014-86-K-0689. Chandru was also supported by NSF grant number DMC 88-07550.The authors gratefully acknowledge the partial support of NSF (Grant DMS 89-06870) and AFOSR (Grant 89-0066 and 89-0512).     

The problem of explaining the disparate performance of hyperresolution and paramodulation

This article is the sixth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the effectiveness of hyperresolution versus that of paramodulation. The problem proposed for research asks one to find the properties that explain why paramodulation is so much more effective than hyperresolution is for solving various problems from algebra. Fore evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

Inference flexibility in Horn clause knowledge bases and the simplex method

This paper shows that the basis matrix inverse of the linear program associated with a propositional Horn clause knowledge base provides a proof structure of inference by forward chaining. The basis matrix inverse indicates how each assertion determines the others and is itself determined by the others. This tabulated proof structure provides a convenient way of making inference transparent and flexible.     

Tree automata with equality constraints modulo equational theories

This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.     

The problem of finding a strategy to control binary paramodulation

This article is the fifth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the equality relation which is so vital to many applications of automated reasoning. The prolem proposed for research asks one to find a strategy for controlling the application of binary paramodulation. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

Recognition of Simple Enlarged Horn Formulas and Simple Extended Horn Formulas

The enlarged Horn formulas generalize the extended Horn formulas introduced by Chandru and Hooker (1991). Their satisfying truth assignments can be generated with polynomial delay. Unfortunately no polynomial algorithm is known for recognizing enlarged Horn formulas or extended Horn formulas. In this paper we define the class of simple enlarged Horn formulas, a subclass of the enlarged Horn formulas, that contains the simple extended Horn formulas introduced by Swaminathan and Wagner (1995). We present recognition algorithms for the simple enlarged Horn formulas and the simple extended Horn formulas whose complexity is bounded by the complexity of the arborescence-realization problem.     

模糊Horn子句规则及其发现算法

模糊Horn子句规则可以用自然语言来表达人类知识。但是,发现模糊Horn子句规则及其蕴含度是比较困难的。该文从逻辑的观点出发,定义模糊Horn子句规则、支持度、蕴含度及其相关概念,分析模糊Horn子句规则发现的步骤,并给出发现算法的形式化描述。该算法结合了模糊Horn子句逻辑概念和Apriori发现算法,从给定的数量型数据库中发现模糊Horn子句规则。     

Semantic foundations for generalized rewrite theories

Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications.     

Formula databases for high-performance resolution/paramodulation systems

Over the past 25 years, researchers have written numerous deduction systems based on resolution and paramodulation. Of these systems, very few have been capable of generating and maintaining aformula database containing more than just a few thousand clauses. These few systems were used to explore mechanisms for rapidly extracting limited subsets of relevant clauses. We have developed a simple, powerful deduction system that reflects some of the best of the ideas that have emerged from the research. This paper describes that deduction system and casts the idea in a form that makes them easily accessible to researchers wishing to write their own high-performance systems.This work was partially supported by National Science Foundation grant CCR-8810947 and by the Office of Scientific Computing, U.S. Department of Energy under contract W-31-109-Eng-38.     

An algorithm to compute maximal contractions for Horn clauses

In the theory of belief revision, the computation of all maximal subsets (maximal contractions) of a formula set with respect to a set of facts is one of the key problems. In this paper, we try to solve this problem by studying the algorithm to compute all maximal contractions for Horn clauses. First, we point out and prove the conversion relationship between minimal inconsistent subsets of union of the formula set and the set of facts and maximal contractions of the formula set with respect to th...     

一个在Horn子句中求解极大缩减的算法

在信念修正理论中,一个核心问题是求解一个公式集合关于事实集合的所有极大协调子集,即极大缩减.本文尝试从算法的角度来解决这一问题,研究在Horn子句中求解所有极大缩减的算法.首先,本文指出并证明了公式集合和事实集合并集的极小不协调子集与公式集合关于事实集合的极大缩减之间的转化关系.其次,给出并证明了Horn子句集合极小不协调的一个必要条件.然后,基于上述两个结论,本文提出了一个在Horn子句中枚举公式集合和事实集合并集的极小不协调子集的交互式算法和一个通过这些极小不协调子集计算所有极大缩减的算法.最后,综合这两个算法,提出了一个在Horn子句中求解所有极大缩减的交互式算法.     

Learning Function-Free Horn Expressions

The problem of learning universally quantified function free first order Horn expressions is studied. Several models of learning from equivalence and membership queries are considered, including the model where interpretations are examples (Learning from Interpretations), the model where clauses are examples (Learning from Entailment), models where extensional or intentional background knowledge is given to the learner (as done in Inductive Logic Programming), and the model where the reasoning performance of the learner rather than identification is of interest (Learning to Reason). We present learning algorithms for all these tasks for the class of universally quantified function free Horn expressions. The algorithms are polynomial in the number of predicate symbols in the language and the number of clauses in the target Horn expression but exponential in the arity of predicates and the number of universally quantified variables. We also provide lower bounds for these tasks by way of characterising the VC-dimension of this class of expressions. The exponential dependence on the number of variables is the main gap between the lower and upper bounds.     

安全协议的扩展Horn逻辑模型及其验证方法

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．     

Polynomial-time inference of all valid implications for Horn and related formulae

This paper investigates the complexity of a general inference problem: given a propositional formula in conjunctive normal form, find all prime implications of the formula. Here, a prime implication means a minimal clause whose validity is implied by the validity of the formula. We show that, under some reasonable assumptions, this problem can be solved in time polynomially bounded in the size of the input and in the number of prime implications. In the case of Horn formulae, the result specializes to yield an algorithm whose complexity grows only linearly with the number of prime implications. The result also applies to a class of formulae generalizing both Horn and quadratic formulae.To the memory of Robert G. Jeroslow     

Inductive expansion: A calculus for verifying and synthesizing functional and logic programs

Guarded Horn clauses over a many-sorted polymorphic signature provide a powerful syntax for design specifications. Expressed as a set of positive Gentzen clauses with a common guard, requirements to such a specification can be proved top-down by inductive expansion: conclusions and generators of the clauses are transformed via resolution and paramodulation upon axioms, lemmas and induction hypotheses into the guard. Case distinctions are generated when axioms or lemmas are applied in parallel. They split the proof into subexpansions, which are later rejoined by applying disjunctive lemmas. Induction orderings need not be selected before redices for induction hypotheses have been created.The controlled expansion of requirements to a function (or predicate) may produce axioms representing a program for that function. This generalizes traditional approaches to program synthesis such as fold& unfold, divide&conquer or deductive tableaus. Ground confluent and strongly terminating design specifications yield decidable criteria for constructors and unsolvable goals and thus reduce the search space of inductive expansion.     

Horn-Extended DL的Tableau算法研究

描述逻辑和逻辑程序是两种非常重要的知识表达形式,分别具有不同的表达能力。为了保证结合描述逻辑和逻辑程序的可判定性,Motik给出了一种DL-safe规则。在Motik工作的基础上,提出了对描述逻辑进行Horn子句拓展的Horn-Extended DL,并给出了Horn-Extended DL的Tableau算法,最后通过一个算例验证了算法的正确性和效率。     

Solution of the Robbins Problem

In this article we show that the three equations known as commutativity,associativity, and the Robbins equation are a basis for the variety ofBoolean algebras. The problem was posed by Herbert Robbins in the 1930s. Theproof was found automatically by EQP, a theorem-proving program forequational logic. We present the proof and the search strategies thatenabled the program to find the proof.     

Learning Horn definitions: Theory and an application to planning

A Horn definition is a set of Horn clauses with the same predicate in all head literals. In this paper, we consider learning non-recursive, first-order Horn definitions from entailment. We show that this class is exactly learnable from equivalence and membership queries. It follows then that this class is PAC learnable using examples and membership queries. Finally, we apply our results to learning control knowledge for efficient planning in the form of goal-decomposition rules. Chandra Reddy, Ph.D.: He is currently a doctoral student in the Department of Computer Science at Oregon State University. He is completing his Ph.D. on June 30, 1998. His dissertation is entitled “Learning Hierarchical Decomposition Rules for Planning: An Inductive Logic Programming Approach.” Earlier, he had an M. Tech in Artificial Intelligence and Robotics from University of Hyderabad, India, and an M.Sc.(tech) in Computer Science from Birla Institute of Technology and Science, India. His current research interests broadly fall under machine learning and planning/scheduling—more specifically, inductive logic programming, speedup learning, data mining, and hierarchical planning and optimization. Prasad Tadepalli, Ph.D.: He has an M.Tech in Computer Science from Indian Institute of Technology, Madras, India and a Ph.D. from Rutgers University, New Brunswick, USA. He joined Oregon State University, Corvallis, as an assistant professor in 1989. He is now an associate professor in the Department of Computer Science of Oregon State University. His main area of research is machine learning, including reinforcement learning, inductive logic programming, and computational learning theory, with applications to classification, planning, scheduling, manufacturing, and information retrieval.