iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositio...
详细信息
ISBN:
(纸本)9783540710691
iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution. In this paper we discuss the design of iProver and related implementation issues.
leanCoP is a very compact theorem prover for classical first-order logic, based on the connection (tableau) calculus and implemented in Prolog. leanCoP 2.0 enhances leanCoP 1.0 by adding regularity, lemmata, and a tec...
详细信息
ISBN:
(纸本)9783540710691
leanCoP is a very compact theorem prover for classical first-order logic, based on the connection (tableau) calculus and implemented in Prolog. leanCoP 2.0 enhances leanCoP 1.0 by adding regularity, lemmata, and a technique for restricting backtracking. It also provides a definitional translation into clausal form and integrates "Prolog technology" into a lean theorem prover. ileanCoP is a compact theorem prover for intuitionistic first-order logic and based on the clausal connection calculus for intuitionistic logic. ileanCoP 1.2 extends the classical prover leanCoP 2.0 by adding prefixes and a prefix unification algorithm. We present details of both implementations and evaluate their performance.
We propose a novel method for reasoning in the description logic SHIQ. After a satisfiability preserving transformation from SHIQ to the description logic ALCIb, the obtained ALCIb Tbox T is converted into an ordered ...
详细信息
ISBN:
(纸本)9783540885634
We propose a novel method for reasoning in the description logic SHIQ. After a satisfiability preserving transformation from SHIQ to the description logic ALCIb, the obtained ALCIb Tbox T is converted into an ordered binary decision diagram (OBDD) which represents a canonical model for T. this OBDD is turned into a disjunctive datalog program that can be used for Abox reasoning. the algorithm is worst-case optimal w.r.t. data complexity, and admits easy extensions with DL-safe rules and ground Conjunctive queries.
the composition of most styles of music is governed by rules. the natural statement of these rules is declarative ("the highest and lowest notes in a piece must be separated by a consonant interval") and non...
详细信息
ISBN:
(纸本)9783540899815
the composition of most styles of music is governed by rules. the natural statement of these rules is declarative ("the highest and lowest notes in a piece must be separated by a consonant interval") and non deterministic ("the base note of a key can be followed by any note in the key"). We show that by approaching the automation and analysis of composition as a knowledge representation task and formalising these rules in a suitable logical language, powerful and expressive intelligent composition tools can easily be built. this paper describes the use of answer set programming to construct an automated system that can compose both melodic and harmonic music, diagnose errors in human compositions and serve as a computer-aided composition tool. the use of a fully declarative language and an "off-the-shelf" reasoning engine allows the creation of tools which are significantly simpler, smaller and more flexible than those produced by existing approaches. It also combines harmonic and melodic composition in a single framework, which is a new feature in the growing area of algorithmic composition.
It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof syste...
详细信息
ISBN:
(纸本)9783540710691
It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof systems. Here, we show that if we adopt different focusing annotations for such linear logic specifications, a range of other proof systems can also be specified. In particular, we show that natural deduction (normal and non-normal), sequent proofs (with and without cut), tableaux, and proof systems using general elimination and general introduction rules can all be derived from essentially the same linear logic specification by altering focusing annotations. By using elementary linear logic equivalences and the completeness of focused proofs, we are able to derive new and modular proofs of the soundness and completeness of these various proofs systems for intuitionistic and classical logics.
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specificat...
详细信息
ISBN:
(纸本)9783540710691
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.
LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate withthe fir...
详细信息
ISBN:
(纸本)9783540710691
LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate withthe first-order automatedtheorem provers E, SPASS, and Vampire. the improved performance of LEO-II, especially in comparison to its predecessor LEO, is due to several novel features including the exploitation of term sharing and term indexing techniques, support for primitive equality reasoning, and improved heuristics at the calculus level. LEO-II is implemented in Objective Caml and its problem representation language is the new TPTP thF language.
Answer set programming provides a powerful platform for model-based reasoning problems. the answer sets are solutions, but for many non-trivial problems post-processing is often necessary for, human readability, In th...
详细信息
ISBN:
(纸本)9783540899815
Answer set programming provides a powerful platform for model-based reasoning problems. the answer sets are solutions, but for many non-trivial problems post-processing is often necessary for, human readability, In this paper we describe a method and a tool for visualising answer sets in which we exploit answer set programming itself to define how visualisations are constructed. Air exciting potential application of our met,hod is to assist in the debugging of answer set programs that,7 as a, consequence, of their declarative nature, are not amendable to traditional approaches: visual rendering of answer sets offers;a way to help programmers spot false and missing solutions,
We consider the problem of computing the logical difference between distinct versions of description logic terminologies. For the lightweight description logic EL, we present a tractable algorithm which, given two ter...
详细信息
ISBN:
(纸本)9783540710691
We consider the problem of computing the logical difference between distinct versions of description logic terminologies. For the lightweight description logic EL, we present a tractable algorithm which, given two terminologies and a signature, outputs a set of concepts, which can be regarded as the logical difference between the two terminologies. As a consequence, the algorithm can also decide whether they imply the same concept implications in the signature. A prototype implementation CEX of this algorithm is presented and experimental results based on distinct versions of SNOMED CT, the Systematized Nomenclature of Medicine, Clinical Terms, are discussed. Finally, results regarding the relation to uniform interpolants and possible extensions to more expressive description logics are presented.
this paper presents a new approach to qualitative spatio-temporal reasoning about movement of mobile agents/objects. We extend spatio-temporal relevant logics by introducing predicates and axiom schemata about movemen...
详细信息
ISBN:
(纸本)9781424420957
this paper presents a new approach to qualitative spatio-temporal reasoning about movement of mobile agents/objects. We extend spatio-temporal relevant logics by introducing predicates and axiom schemata about movement of mobile objects, and defining the notion of distance by predicates about point position and adjacency, predicates about movement of mobile objects, and temporal operators. As a result, the new spatio-temporal relevant logics can be used to represent and reason about movement of mobile agents in the cyberworld as well as mobile objects in the real world.
暂无评论