the paper provides a new approach for automatedreasoning in a logic Program using extended Petri net models. the design includes extension of classical linear resolution of first order logic clauses by multi-resoluti...
详细信息
ISBN:
(纸本)0769530508
the paper provides a new approach for automatedreasoning in a logic Program using extended Petri net models. the design includes extension of classical linear resolution of first order logic clauses by multi-resolution, where a set of clauses can be resolved concurrently without sacrificing any inference, thereby speeding-up the execution of the logic program. the speed-tip and utilization rate of resources are used as the performance evaluation metric to compare the performance of the proposed system withthe classical one.
reasoning on Constraint Handling Rules (CHR) programs and their executional behaviour is often ad-hoc and outside of a formal system. this is a pity, because CHR subsumes a wide range of important automatedreasoning ...
详细信息
ISBN:
(纸本)9783540721994
reasoning on Constraint Handling Rules (CHR) programs and their executional behaviour is often ad-hoc and outside of a formal system. this is a pity, because CHR subsumes a wide range of important automatedreasoning services. Mapping CHR to Transaction logic (TR) combines CHR rule specification, CHR rule application, and reasoning on CHR programs and CHR derivations inside one formal system which is executable. this new TR semantics obviates the need for disjoint declarative and operational semantics.
We present Zenon, an automatedtheorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented alg...
详细信息
ISBN:
(纸本)9783540755586
We present Zenon, an automatedtheorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.
the goal of this article is to formalize Object Role Modeling (ORM) using the DLR description logic. this would enable automatedreasoning on the formal properties of ORM diagrams, such as detecting constraint contrad...
详细信息
ISBN:
(纸本)9783540755623
the goal of this article is to formalize Object Role Modeling (ORM) using the DLR description logic. this would enable automatedreasoning on the formal properties of ORM diagrams, such as detecting constraint contradictions and implications. In addition, the expressive, methodological, and graphical capabilities of ORM make it a good candidate for use as a graphical notation for most description logic languages. In this way, industrial experts who are not IT savvy will still be able to build and view axiomatized theories (such as ontologies, business rules, etc.) without needing to know the logic or reasoning foundations underpinning them. Our formalization in this paper is structured as 29 formalization rules, that map all ORM primitives and constraints into DLR, and 2 exceptions of complex cases. To this end, we illustrate the implementation of our formalization as an extension to DogmaModeler, which automatically maps ORM into DIG and uses Racer as a background reasoning engine to reason about ORM diagrams.
Since the early days of AI, automatedreasoning has been a rather elusive goal. In fact, up till the early nineties, general inference beyond hundred variable problems appeared infeasible. Over the last decade, we hav...
详细信息
ISBN:
(纸本)9783540738466
Since the early days of AI, automatedreasoning has been a rather elusive goal. In fact, up till the early nineties, general inference beyond hundred variable problems appeared infeasible. Over the last decade, we have witness a qualitative change in the field: current reasoning engines can handle problems with over a million variables and several millions of constraints. I will discuss what led to such a dramatic scale-up, and how progress in reasoning technology has opened up a range of new applications in AI and computer science in general. I will also discuss initial progress on the use of learning techniques in reasoning engines and the remaining challenges for obtaining a true integration of learning and reasoning.
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and Nonmonotonic reasoning. the aims of the c...
详细信息
ISBN:
(纸本)9783540721994
this paper gives a summary of the First Answer Set programming System Competition that was held in conjunction withthe Ninthinternationalconference on logicprogramming and Nonmonotonic reasoning. the aims of the competition were twofold: first, to collect challenging benchmark problems, and second, to provide a platform to assess a broad variety of Answer Set programming systems. the competition was inspired by similar events in neighboring fields, where regular benchmarking has been a major factor behind improvements in the developed systems and their ability to address practical applications.
We show how to deploy the CIFF System 4.0 for abductive logicprogramming with constraints in a number of applications, ranging from combinatorial applications to web management. We also compare the CIFF System 4.0 wi...
详细信息
ISBN:
(纸本)9783540721994
We show how to deploy the CIFF System 4.0 for abductive logicprogramming with constraints in a number of applications, ranging from combinatorial applications to web management. We also compare the CIFF System 4.0 with a number of logicprogramming tools, namely the A-System, the DLV system and the SMODELS system.
We introduce a sequent calculus for bilattice-based annotated logic (BAL). We show that this logic can be syntactically and semantically translated into a fragment MSL* of conventional many-sorted logic MSL. We show d...
详细信息
ISBN:
(纸本)9783540730989
We introduce a sequent calculus for bilattice-based annotated logic (BAL). We show that this logic can be syntactically and semantically translated into a fragment MSL* of conventional many-sorted logic MSL. We show deductive equivalence of sequent calculus for BAL and sequent calculus for MSL*.
We describe the development of a constraint logicprogramming based system, called CPP, which is capable of generating most preferred plans with respect to a user's preference and evaluate its performance.
ISBN:
(纸本)9783540721994
We describe the development of a constraint logicprogramming based system, called CPP, which is capable of generating most preferred plans with respect to a user's preference and evaluate its performance.
We describe a new grounder system for logic programs under answer set semantics, called GrinGo. Our approach combines and extends techniques from the two primary grounding approaches of lparse and dlv. A major emphasi...
详细信息
ISBN:
(纸本)9783540721994
We describe a new grounder system for logic programs under answer set semantics, called GrinGo. Our approach combines and extends techniques from the two primary grounding approaches of lparse and dlv. A major emphasis lies on an extensible design that allows for an easy incorporation of new language features in an efficient system environment.
暂无评论