this is a technical report that outlines and highlights functional and non functional requirements for modelling and building strategy games. the report covers language definitions, heuristics for choosing a computer ...
详细信息
ISBN:
(纸本)9780954901660
this is a technical report that outlines and highlights functional and non functional requirements for modelling and building strategy games. the report covers language definitions, heuristics for choosing a computer language, generations of programming languages, criteria for heuristics and a heuristics model. the requirements captured and analysed also focus on the different game modes, the game play, graphics, audio, controls, and the user interface. the requirements have been automated using horn clause logic and deployed in Visual Prolog 7.
Modular cut-elimination is a particular notion of "cut-elimination in the presence of non-logical axioms" that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficie...
详细信息
ISBN:
(纸本)3540482814
Modular cut-elimination is a particular notion of "cut-elimination in the presence of non-logical axioms" that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficient conditions for modular cut-elimination for standard calculi, a wide class of (possibly) multiple-conclusion sequent calculi with generalized quantifiers. We provide a "universal" modular cut-elimination procedure that works uniformly for any standard calculus satisfying our conditions. the failure of these conditions generates counterexamples for modular cut-elimination and, in certain cases, for cut-elimination.
inductivelogicprogramming (ILP) is an inductive reasoning method based on the first-order predicative logic. this technology is widely used for data mining using symbolic artificial intelligence. ILP searches for a ...
详细信息
ISBN:
(纸本)9783031291258;9783031291265
inductivelogicprogramming (ILP) is an inductive reasoning method based on the first-order predicative logic. this technology is widely used for data mining using symbolic artificial intelligence. ILP searches for a suitable hypothesis that covers positive examples and uncovers negative examples. the searching process requires a lot of execution cost to interpret many given examples for practical problems. In this paper, we propose a new hypothesis search method using particle swarm optimization (PSO). PSO is a meta-heuristic algorithm based on behaviors of particles. In our approach, each particle repeatedly moves from a hypothesis to another hypothesis within a hypothesis space. At that time, some hypotheses are refined based on the value returned by a predefined evaluation function. Since PSO just searches a part of the hypothesis space, it contributes to the speed up of the execution of ILP. In order to demonstrate the effectiveness of our method, we have implemented it on Progol that is one of the ILP systems [6], and then we conducted numerical experiments. the results showed that our method reduced the hypothesis search time compared to another conventional Progol.
We explain why the original proofs of P-Time completeness for Light Affine logic and Light Linear logic can not work, and we fully develop a working one.
ISBN:
(纸本)3540665366
We explain why the original proofs of P-Time completeness for Light Affine logic and Light Linear logic can not work, and we fully develop a working one.
In this paper we present a new method that uses data-flow coherence criteria in definite logic program generation. We outline three main advantages of these criteria supported by our results: i) drastically pruning th...
详细信息
ISBN:
(纸本)0769514170
In this paper we present a new method that uses data-flow coherence criteria in definite logic program generation. We outline three main advantages of these criteria supported by our results: i) drastically pruning the search space (around 90%), ii) reducing the set of positive examples and reducing or even removing the need for the set of negative examples, and iii) allowing the induction of predicates that are difficult or even impossible to generate by other methods. Besides these criteria, the approach takes into consideration the program termination condition for recursive predicates. the paper outlines some theoretical issues and implementation aspects of our system for automatic logic program induction.
We present an approach for computing intensional answers given a set of extensional answers returned as a result of a user query to an information system. Intensional answers are considered as descriptions of the actu...
详细信息
ISBN:
(纸本)9783540698579
We present an approach for computing intensional answers given a set of extensional answers returned as a result of a user query to an information system. Intensional answers are considered as descriptions of the actual answers in terms of properties they share and which can enhance a user's understanding of the answer itself but also of the underlying knowledge base. In our approach, an intensional answer is represented by a clause and computed based on inductivelogicprogramming (ILP) techniques, in particular bottom-up clause generalization. the approach is evaluated in terms of usefulness and time performance, and its potential for helping to detect flaws in the knowledge base is discussed. While the approach is used in the context of a natural language question answering system in our setting, it clearly has applications beyond.
In this paper we present a method of integrating theory reasoning into the instantiation framework. this integration is done in the black-box style, which allows us to integrate different theories in a uniform way. We...
详细信息
ISBN:
(纸本)3540482814
In this paper we present a method of integrating theory reasoning into the instantiation framework. this integration is done in the black-box style, which allows us to integrate different theories in a uniform way. We prove completeness of the resulting calculus, provided that the theory reasoner is answer-complete and complete for reasoning with ground clauses. One of the distinctive features of our approach is that it allows us to employ off-the-shelf satisfiability solvers for ground clauses modulo theories, as a part of general first-order reasoning. As an application of this approach, we show how it is possible to combine the instantiation calculus with other calculi, such as ordered resolution and paramodulation.
We present a definition of untyped lambda -terms using a heterogeneous datatype, i.e. an inductively defined operator. this operator can be extended to a Kleish triple, which is a concise way to verify the substitutio...
详细信息
ISBN:
(纸本)3540665366
We present a definition of untyped lambda -terms using a heterogeneous datatype, i.e. an inductively defined operator. this operator can be extended to a Kleish triple, which is a concise way to verify the substitution laws for lambda -calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed lambda -calculus using dependent types, and show that this is an instance of a generalization of Kleish triples. the proofs for the untyped case have been checked using the LEGO system.
暂无评论