共查询到20条相似文献,搜索用时 31 毫秒
1.
Modern explanatory inductive logic programming methods like Progol, Residue procedure, CF-induction, HAIL and Imparo use the
principle of inverse entailment (IE). Those IE-based methods commonly compute a hypothesis in two steps: by first constructing
an intermediate theory and next by generalizing its negation into the hypothesis with the inverse of the entailment relation.
Inverse entailment ensures the completeness of generalization. On the other hand, it imposes many non-deterministic generalization
operators that cause the search space to be very large. For this reason, most of those methods use the inverse relation of
subsumption, instead of entailment. However, it is not clear how this logical reduction affects the completeness of generalization.
In this paper, we investigate whether or not inverse subsumption can be embedded in a complete induction procedure; and if
it can, how it is to be realized. Our main result is a new form of inverse subsumption that ensures the completeness of generalization.
Consequently, inverse entailment can be reduced to inverse subsumption without losing the completeness for finding hypotheses
in explanatory induction. 相似文献
2.
Peter Padawitz 《Journal of Automated Reasoning》1991,7(1):27-103
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. 相似文献
3.
Declarative Bias for Specific-to-General ILP Systems 总被引:1,自引:1,他引:0
A comparative study is presented of language biases employed in specific-to-general learning systems within the Inductive Logic Programming (ILP) paradigm. More specifically, we focus on the biases employed in three well known systems: CLINT, GOLEM and ITOU, and evaluate both conceptually and empirically their strengths and weaknesses. The evaluation is carried out within the generic framework of the NINA system, in which bias is a parameter. Two different types of biases are considered: syntactic bias, which defines the set of well-formed clauses, and semantic bias, which imposes restrictions on the behaviour of hypotheses or clauses. NINA is also able to shift its bias (within a predefined series of biases), whenever its current bias is insufficient for finding complete and consistent concept definitions. Furthermore, a new formalism for specifying the syntactic bias of inductive logic programming systems is introduced.This paper extends the papers (Adé & Bruynooghe, 1992) and (Rouveirol et al., 1993). 相似文献
4.
在扩展规则的基础上提出了可能性扩展规则。给出了基于可能性扩展规则的可能性逻辑推理方法,利用互补因子的概念来估价推理问题的复杂度。扩展了经典逻辑的蕴含可控制类和可满足可控制类的定义,提出了可能性蕴含可控制类、不一致性程度计算可控制类的概念。在可能性扩展规则的基础上提出了EPPCCCL(each pair of possibilistic clauses contains complementary literals)理论,并证明了该理论是在最优化形式蕴含可控制类和不一致性程度计算可控制类中的,可以作为可能性 相似文献
5.
Hypotheses constructed by inductive logic programming (ILP) systems are finite sets of definite clauses. Top-down ILP systems
usually adopt the following greedy clause-at-a-time strategy to construct such a hypothesis: start with the empty set of clauses
and repeatedly add the clause that most improves the quality of the set. This paper formulates and analyses an alternative
method for constructing hypotheses. The method, calledcautious induction, consists of a first stage, which finds a finite set of candidate clauses, and a second stage, which selects a finite subset
of these clauses to form a hypothesis. By using a less greedy method in the second stage, cautious induction can find hypotheses
of higher quality than can be found with a clause-at-a-time algorithm. We have implemented a top-down, cautious ILP system
called CILS. This paper presents CILS and compares it to Progol, a top-down clause-at-a-time ILP system. The sizes of the
search spaces confronted by the two systems are analysed and an experiment examines their performance on a series of mutagenesis
learning problems.
Simon Anthony, BEng.: Simon, perhaps better known as “Mr. Cautious” in Inductive Logic Programming (ILP) circles, completed a BEng in Information
Engineering at the University of York in 1995. He remained at York as a research student in the Intelligent Systems Group.
Concentrating on ILP, his research interests are Cautious Induction and developing number handling techniques using Constraint
Logic Programming.
Alan M. Frisch, Ph.D.: He is the Reader in Intelligent Systems at the University of York (UK), and he heads the Intelligent Systems Group in the
Department of Computer Science. He was awarded a Ph. D. in Computer Science from the University of Rochester (USA) in 1986
and has held faculty positions at the University of Sussex (UK) and the University of Illinois at Urbana-Champaign (USA).
For over 15 years Dr. Frisch has been conducting research on a wide range of topics in the area of automated reasoning, including
knowledge retrieval, probabilistic inference, constraint solving, parsing as deduction, inductive logic programming and the
integration of constraint solvers into automated deduction systems. 相似文献
6.
Timothy R. Colburn 《Minds and Machines》1991,1(4):417-436
The general conditions of epistemic defeat are naturally represented through the interplay of two distinct kinds of entailment, deductive and defeasible. Many of the current approaches to modeling defeasible reasoning seek to define defeasible entailment via model-theoretic notions like truth and satisfiability, which, I argue, fails to capture this fundamental distinction between truthpreserving and justification-preserving entailments. I present an alternative account of defeasible entailment and show how logic programming offers a paradigm in which the distinction can be captured, allowing for the modeling of a larger range of types of defeat. This is possible through a natural extension of the declarative and procedural semantics of Horn clauses. 相似文献
7.
In Inductive Logic Programming (ILP), algorithms that are purely of the bottom-up or top-down type encounter several problems in practice. Since a majority of them are greedy ones, these algorithms stop when finding clauses in local optima, according to the “quality” measure used for evaluating the results. Moreover, when learning clauses one by one, the induced clauses become less and less interesting as the algorithm is progressing to cover few remaining examples. In this paper, we propose a simulated annealing framework to overcome these problems. Using a refinement operator, we define neighborhood relations on clauses and on hypotheses (i.e. sets of clauses). With these relations and appropriate quality measures, we show how to induce clauses (in a coverage approach), or to induce hypotheses directly by using simulated annealing algorithms. We discuss the necessary conditions on the refinement operators and the evaluation measures to increase the effectiveness of the algorithm. Implementations (included a parallelized version of the algorithm) are described and experimentation results in terms of convergence of the method and in terms of accuracy are presented. 相似文献
8.
During incremental concept learning from examples, tentative hypotheses are formed and then modified to form new hypotheses. When there is a choice among hypotheses, bias is used to express a preference. Bias may be expressed by the choice of hypothesis language, it may be implemented as an evaluation function for selecting among hypotheses already generated, or it may consist of screening potential hypotheses prior to hypothesis generation. This paper describes the use of the third method. Bias is represented explicitly both as assumptions that reduce the space of potential hypotheses and as procedures for testing these assumptions. There are advantages gained by using explicit assumptions. One advantage is that the assumptions are meta-level hypotheses that are used to generate future, as well as to select between current, inductive hypotheses. By testing these meta-level hypotheses, a system gains the power to anticipate the form of future hypotheses. Furthermore, rigorous testing of these meta-level hypotheses before using them to generate inductive hypotheses avoids consistency checks of the inductive hypotheses. A second advantage of using explicit assumptions is that bias can be tested using a variety of learning methods. 相似文献
9.
Constantin Enea Ondřej Lengál Mihaela Sighireanu Tomáš Vojnar 《Formal Methods in System Design》2017,51(3):575-607
We present a decision procedure for checking entailment between separation logic formulas with inductive predicates specifying complex data structures corresponding to finite nesting of various kinds of singly linked lists: acyclic or cyclic, nested lists, skip lists, etc. The decision procedure is compositional in the sense that it reduces the problem of checking entailment between two arbitrary formulas to the problem of checking entailment between a formula and an atom. Subsequently, in case the atom is a predicate, we reduce the entailment to testing membership of a tree derived from the formula in the language of a tree automaton derived from the predicate. The procedure is later also extended to doubly linked lists. We implemented this decision procedure and tested it successfully on verification conditions obtained from programs using both singly and doubly linked nested lists as well as skip lists. 相似文献
10.
11.
Bottom-Up Induction of Feature Terms 总被引:2,自引:0,他引:2
The aim of relational learning is to develop methods for the induction of hypotheses in representation formalisms that are more expressive than attribute-value representation. Most work on relational learning has been focused on induction in subsets of first order logic like Horn clauses. In this paper we introduce the representation formalism based on feature terms and we introduce the corresponding notions of subsumption and anti-unification. Then we explain INDIE, a heuristic bottom-up learning method that induces class hypotheses, in the form of feature terms, from positive and negative examples. The biases used in INDIE while searching the hypothesis space are explained while describing INDIE's algorithms. The representational bias of INDIE can be summarised in that it makes an intensive use of sorts and sort hierarchy, and in that it does not use negation but focuses on detecting path equalities. We show the results of INDIE in some classical relational datasets showing that it's able to find hypotheses at a level comparable to the original ones. The differences between INDIE's hypotheses and those of the other systems are explained by the bias in searching the hypothesis space and on the representational bias of the hypothesis language of each system. 相似文献
12.
13.
Clausal Discovery 总被引:5,自引:0,他引:5
14.
15.
Several well-known inductive inference strategies change the actual hypothesis only when they discover that it "provably misclassifies" an example seen so far. This notion is made mathematically precise, and its general power is characterized. In spite of its strength, it is shown that this approach is not of universal power. Consequently, hypotheses are considered which "unprovably misclassify" examples, and the properties of this approach are studied. Among others, it turns out that this type is of the same power as monotonic identification. Then it is shown that universal power can be achieved only when an unbounded number of alternations of these dual types of hypotheses is allowed. Finally, a universal method is presented, enabling an inductive inference strategy to verify the incorrectness of any of its incorrect intermediate hypotheses. 相似文献
16.
《IEEE transactions on pattern analysis and machine intelligence》1976,(4):244-252
We will consider the inductive mechanisms in five techniques for verifying iterative/recursive program structures: inductive assertion, predicate transformers, subgoal induction, computation induction, and structural induction. We will discover that all five techniques can be justified by a single theorem about inductive proof techniques. We will also show that all five techniques face the problem of finding properties that will carry an induction. Such properties are called inductive sets. We will see that the inductive sets of the five techniques are easily related to one another and that a program proof by any of the techniques can be easily converted to a proof by any of the other techniques. Our conclusion is that computer programs simply are inductive definitions of the functions they compute. Induction is the only method by which they can be proved. The problems of induction are therefore unavoidable. 相似文献
17.
18.
归纳逻辑程序设计的核心问题是如何从背景知识中优选谓词构造满足约束的归纳假设,按Occam准则,满足约束的最精简归纳假设为优,但迄今归纳逻辑程序设计中精简归纳假设构造的计算复杂性尚未解决。 相似文献
19.
为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器(GLUCOSE 4.1并行版本)为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。 相似文献
20.
《Information Fusion》2003,4(1):47-61
Plan recognition can roughly be described as the problem of finding the plan(s) underlying the observed behaviour of agent(s). Of course, usually, the observed behaviour and available background knowledge does not determine the underlying plan, and therefore one can typically at best generate (reasonable) plan hypotheses. Traditionally, plan recognition has been studied, formalized and implemented in areas like story understanding and user modelling. In this paper, we propose a formal definition of tactical plan recognition, i.e. the recognition of enemy plans. We will focus on military applications, where this task of tactical plan recognition is crucial, but this task is relevant for every application where one has to deal with intelligent adversial agents.Tactical plan recognition differs from traditional plan recognition in a number of ways. For example, an enemy will often try to avoid making his plans known. We will not pay much explicit attention to this feature. We will focus on another important characteristic feature of tactical plan recognition, namely that the identity of the observed enemy objects, for which plans are to be recognized, may be unknown. A consequence of this is that it is typically not known which observations originate from the same objects.Our formalization of plan recognition is based on classical abduction. The concepts of classical abduction can readily be applied to plan recognizers for identified observations, as has been done by Lin and Goebel [18] and Bauer and Paul [7]. However, for tactical plan recognition some adaptations have to be made. Here the plan recognizer will not only have to generate plan hypotheses, but also assignment hypotheses, which correspond to formal links of objects to observations. A choice for an assignment is essentially a decision concerning the question which observations originate from the same objects.For observations with stochastic variables the probability of an assignment hypothesis is calculated, rather than the probability of the plan hypotheses. For this, Reid’s multiple hypothesis tracking formula can be adapted to calculate the assignment hypothesis probability. 相似文献