For many years all known completeness results for Knuth- Bendix completion and ordered paramodulation required the term ordering γ to be well-founded, monotonic and total(izable) on ground terms. then, it was shown t...
详细信息
In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can als...
详细信息
Prolog has been used as an inference engine of many systems, and it is natural to use Prolog as an inference engine of intelligent agent systems. However, Prolog assumes that a program does not change. this poses a pr...
详细信息
ISBN:
(纸本)3540439307
Prolog has been used as an inference engine of many systems, and it is natural to use Prolog as an inference engine of intelligent agent systems. However, Prolog assumes that a program does not change. this poses a problem because the agent might work in a dynamic environment where unexpected things can happen. In order to use a Prolog-like procedure as an inference engine of an agent, the procedure should be able to modify the computation, if necessary, after updating the program or executing an action. We introduce a new Prolog-like procedure which integrates planning, action execution, program updates, and plan modifications. Our new procedure computes plans by abduction. During or after a computation, it can update a program by adding a rule to the program or deleting a rule from the program. After updating the program, it modifies the computation, cuts invalid plans, and adds new valid plans. We use the technique of Dynamic SLDNF (DSLDNF) [1] [2] to modify computation after updating a program. It is also possible to execute an action during or after planning. We can use three types of actions: an action without a side effect; an action with a side effect which can be undone; an action with a side effect which cannot be undone. Following the result of action execution, the procedure modifies the computation: invalid plans are erased; some actions are undone; some redundant actions are erased. Even if a plan becomes invalid, it is possible to switch to another plan without loss of correctness. Based on the technique described above, we implemented an intelligent mobile network agent system, pi-coPlangent.
Markov logic Networks (MLNs) combine Markov networks and first-order logic by attaching weights to first-order formulas and viewing these as templates for features of Markov networks. Learning the structure of MLNs is...
详细信息
ISBN:
(纸本)9783540859277
Markov logic Networks (MLNs) combine Markov networks and first-order logic by attaching weights to first-order formulas and viewing these as templates for features of Markov networks. Learning the structure of MLNs is performed by state-of-the-art methods by maximizing the likelihood of a relational database. this can lead to suboptimal results given prediction tasks. On the other hand better results in prediction problems have been achieved by discriminative learning of MLNs weights given a certain structure. In this paper we propose an algorithm for learning the structure of MLNs discriminatively by maximimizing the conditional likelihood of the query predicates instead of the joint likelihood of all predicates. the algorithm chooses the structures by maximizing conditional likelihood and sets the parameters by maximum likelihood. Experiments in two real-world domains show that the proposed algorithm improves over the state-of-the-art discriminative weight learning algorithm for MLNs in terms of conditional likelihood. We also compare the proposed algorithm withthe state-of-the-art generative structure learning algorithm for MLNs and confirm the results ill [22] showing that for small datasets the generative algorithm is competitive, while for larger datasets the discriminative algorithm outperfoms the generative one.
We identify a shortcoming of a standard positive-only clause evaluation function within the context of learning biological grammars. To overcome this shortcoming we propose L-modification, a modification to this evalu...
详细信息
ISBN:
(纸本)9783540859277
We identify a shortcoming of a standard positive-only clause evaluation function within the context of learning biological grammars. To overcome this shortcoming we propose L-modification, a modification to this evaluation function such that the lengths of individual examples are considered. We use a set of bio-sequences known as neuropeptide precursor middles (NPP-middles). Using L-modification to learn from these NPP-middles results in induced grammars that have a better performance than that achieved when using the standard positive-only clause evaluation function. We also show that L-modification improves the performance of induced grammars when learning on short, medium or long NPPs-middles. A potential disadvantage of L-modification is discussed. Finally, we show that, as the limit on the search space size increases, the greater is the increase in predictive performance arising from L-modification.
Debugging is a laborious part of the software development process as well as of programming education. Although existing editors and IDEs support the identification of syntax errors, their functions for detecting logi...
详细信息
Spass is an automated theorem prover for full first-order logic with equality. this system description provides an overview of recent developments in Spass 2.0, including among others an implementation of contextual r...
详细信息
the proceedings contain 15 papers. the topics discussed include: on optimising shape-generic array programs using symbolic structural information;index vector elimination-making index vectors affordable;functional-bas...
详细信息
ISBN:
(纸本)9783540741299
the proceedings contain 15 papers. the topics discussed include: on optimising shape-generic array programs using symbolic structural information;index vector elimination-making index vectors affordable;functional-based synthesis of a systolic array for GCD computation;comparing alternative evaluation strategies for stream-based parallel functional languages;parallel coordination made explicit in a functional setting;a conference management system based on the iData toolkit;a pattern logic for prompt lazy assertions in Haskell;IVOR,a proof engine;proving program properties specified with subtype marks;uniqueness typing redefined;heuristics for type error discovery and recovery;testing properties of generic functions;worst-case execution times for a purely functional language;and automatic partial inversion of inductively sequential functions.
In the wider perspective of narrowing down some of the gaps that prevent the adoption of declarative logicprogramming within highly dynamically changing environments, we focus in this paper on the context of integrat...
详细信息
ISBN:
(纸本)9783030351663;9783030351656
In the wider perspective of narrowing down some of the gaps that prevent the adoption of declarative logicprogramming within highly dynamically changing environments, we focus in this paper on the context of integrating reasoning modules in real-time videogames. Integrating rule-based AI within the commercial game development life-cycle poses a number of unsolved challenges, each with non-obvious solution. For instance, it is necessary to cope with strict time performance requirements;the duality between procedural code and declarative specifications prevents easy integration;the concurrent execution of reasoning tasks and game updates requires proper information passing strategies between the two involved sides. In this work we illustrate our recent progress on how to embed rule-based reasoning modules into the well-known Unity game development engine. To this end, we report about thinkEngine, a framework in which a tight integration of declarative formalisms within the typical game development workflow is made possible. We prove the viability of our approach by developing a proof-of-concept Unity game that makes use of ASP-based AI modules.
Proof-carrying code (PCC)is a framework for ensuring that untrusted programs are safe to install and execute. When using PCC, untrusted programs are required to contain a proof that allows the program text to be check...
详细信息
暂无评论