In order to capture the full fledge semantic of complicated product data model, the expressive language ALCNHR+K(D) is introduced. It cannot only be able to represent knowledge about concrete domain and constraints, b...
详细信息
ISBN:
(纸本)1595931120
In order to capture the full fledge semantic of complicated product data model, the expressive language ALCNHR+K(D) is introduced. It cannot only be able to represent knowledge about concrete domain and constraints, but also rules in some sense of closed world semantic model hypothesis. Also the paper investigates an extension to description logic (DL) based knowledge reasoning by means of decomposing and rewriting complicated hybrid concepts into partitions. We present an approach that automatically decomposes the whole knowledge base into description logic compatible one and constraints solver one. Our arguments are two-fold. First, complex DLs with powerful representation ability lack effective reasoning ability. Second, we are concerned with how to reason effectively withthe combination of inferences from distributed heterogeneous reasoner.
Given two classes of logic programs, we may be interested in modular translations from one class into the other that are sound with respect to the answer set semantics. the main theorem of this paper characterizes the...
详细信息
ISBN:
(纸本)3540285385
Given two classes of logic programs, we may be interested in modular translations from one class into the other that are sound with respect to the answer set semantics. the main theorem of this paper characterizes the existence of such a translation in terms of strong equivalence. the theorem is used to study the expressiveness of several classes of programs, including the comparison of cardinality constraints with monotone cardinality atoms.
In this paper a, proof technique for reasoning about the multimodal logic of beliefs and goals is defined based on resolution at different levels of a. tree of clauses. We have considered belief and goal as normal mod...
详细信息
ISBN:
(纸本)3540252363
In this paper a, proof technique for reasoning about the multimodal logic of beliefs and goals is defined based on resolution at different levels of a. tree of clauses. We have considered belief and goal as normal modal logic operators. the technique is inspired by that in [6,7] and allows for a locality property to be satisfied. the main motivation for this work arises not as much from theorem-proving as from the notion of belief and goal revision under an assumption of consistency of the beliefs and goals of an agent. We, also present proofs of soundness and completeness of the logic.
Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipe...
详细信息
ISBN:
(纸本)354030553X
Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipelined processor designs and timed systems, In this paper, we present a fast decision procedure for separation logic, which combines Boolean satisfiability (SAT) with a graph based incremental negative cycle elimination algorithm. Our solver abstracts a separation logic formula into a Boolean formula by replacing each predicate with a Boolean variable. Transitivity constraints over predicates are detected from the constraint graph and added on a need-to basis. Our solver handles Boolean and theory conflicts uniformly at the Boolean level. the graph based algorithm supports not only incremental theory propagation, but also constant time theory backtracking without using a cumbersome history stack. Experimental results on a large set of benchmarks show that our new decision procedure is scalable, and outperforms existing techniques for this logic.
Recently, linear logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear ...
详细信息
ISBN:
(纸本)354030553X
Recently, linear logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear logic can be used to draw conclusions about the specified sequent calculus. For example, derivability of one proof system from another can be decided by a simple procedure that is implemented via bounded logicprogramming-style search. Also, simple and decidable conditions on the linear logic presentation of inference rules, called homogeneous and coherence, can be used to infer that the initial rules can be restricted to atoms and that cuts can be eliminated. In the present paper we introduce Llinda, a logical framework based on linear logic augmented with inference rules for definition (fixed points) and induction. In this way, the above properties can be proved entirely inside the framework. To further illustrate the power of Llinda, we extend the definition of coherence and provide a new, semi-automated proof of cut-elimination for Girard's logic of Unicity (LU).
In recent years much work has been done to find regularities in data streams. Normally streams are complete and well ordered. Major defects, such as incomplete or misleading events, occur in practice at least after so...
详细信息
ISBN:
(纸本)0780392868
In recent years much work has been done to find regularities in data streams. Normally streams are complete and well ordered. Major defects, such as incomplete or misleading events, occur in practice at least after some finite time. In this paper we describe a method developed for recognizing previously known patterns from a data stream. the solution is based on Case Based reasoning (CBR) with an extension to handle imperfect information. We also introduce a new idea to use two different case-bases instead of only one. the performance has been evaluated using simulated data and the obtained results are considered encouraging.
Often graphs are used to investigate properties of logic programs. In general, different graphs represent different kinds of information of the underlying programs. Sometimes this information is not sufficient for sol...
详细信息
ISBN:
(纸本)3540252363
Often graphs are used to investigate properties of logic programs. In general, different graphs represent different kinds of information of the underlying programs. Sometimes this information is not sufficient for solving a certain problem. In this paper we define graphs which are suitable for computing answer sets of logic programs. Intuitively, a graph associated to a logic program is suitable for answer set semantics if its structure is sufficient to compute the answer sets of the corresponding program. We identify different classes of graphs to be suitable for different classes of programs. We also give first experimental results showing the impact of the used graph type to one particular graph based algorithm for answer set computation.
the main goal of this paper is to apply rewriting termination technology-enjoying a quite mature set of termination results and tools-to the problem of proving automatically the termination of concurrent systems under...
详细信息
ISBN:
(纸本)354030553X
the main goal of this paper is to apply rewriting termination technology-enjoying a quite mature set of termination results and tools-to the problem of proving automatically the termination of concurrent systems under fairness assumptions. We adopt the thesis that a concurrent system can be naturally modeled as a rewrite system, and develop a reductionistic theoretical approach to systematically transform, under reasonable assumptions, fair-termination problems into ordinary termination problems of associated relations, to which standard rewriting termination techniques and tools can be applied. Our theoretical results are combined into a practical proof methodology for proving fair-termination that can be automated and can be supported by current termination tools. We illustrate this methodology with some concrete examples and briefly comment on future extensions.
the proceedings contain 33 papers. the topics discussed include: reflecting proofs in first-order logic with equality;tabling for higher-order logicprogramming;simulating reachability using first-order logic with app...
详细信息
ISBN:
(纸本)3540280057
the proceedings contain 33 papers. the topics discussed include: reflecting proofs in first-order logic with equality;tabling for higher-order logicprogramming;simulating reachability using first-order logic with applications to verification of linked data structures;privacy-sensitive information flow with JML;temporal logics over transitive states;hierarchical reasoning in local theory extensions;decision procedures customized for formal verification;connecting many-sorted theories;a proof-producing decision procedure for real arithmetic;the MathSAT 3 system;deduction with XOR constraints in security API modelling;on the complexity of equational horn clauses;and a combination method for generating interpolants.
We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. the central proof-theoretic insights underlying the prover concern resource managem...
详细信息
ISBN:
(纸本)3540280057
We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. the central proof-theoretic insights underlying the prover concern resource management and focused derivations, both of which are traditionally understood in the domain of backward reasoning systems such as logicprogramming. We illustrate how resource management, focusing, and other intrinsic properties of linear connectives affect the basic forward operations of rule application, contraction, and forward subsumption. We also present some preliminary experimental results obtained with our implementation.
暂无评论