Transportation of electrical energy is normally made through a network of hightension lines. In case of an incident, the electrical protections at both ends of a line are activated. Most of the incidents are short-liv...
详细信息
ISBN:
(纸本)9783540220077
Transportation of electrical energy is normally made through a network of hightension lines. In case of an incident, the electrical protections at both ends of a line are activated. Most of the incidents are short-lived, and can be solved by fast automatic reclosure of the breakers. When automatic reclosure fails, or does not happen, a timed reclosure is attempted after a few minutes, either manually or by automatic systems. When an incident occurs, several hundred messages sent by the substations can reach the control centers within a few seconds, making the human operator's interpretation of the incident very difficult. the purpose of the previously developed SPARSE (Expert System for Incident Analysis and Power Restoration Assistance) is to assist the human operators in handling the emergency situations, giving them readable and accurate information. SPARSE is based on a logicprogramming inference engine reasoning over a set of time-stamped events. the new problem we addressed was how to validate the inference rules of SPARSE, by showing that no set of real events and diagnoses could be abduced that would violate the physical and logical integrity constraints of the problem domain, in order to certify the correctness of SPARSE with respect to the desired constraints. In this paper we examine how the sophisticated abductive logicprogramming system ABDUAL was employed for this purpose, and the practical tools developed and implemented to that end.
the proceedings contain 30 papers. the special focus in this conference is on logic for programming, artificialintelligence, and reasoning. the topics include: Improving on-demand strategy annotations;first-order log...
ISBN:
(纸本)3540000100
the proceedings contain 30 papers. the special focus in this conference is on logic for programming, artificialintelligence, and reasoning. the topics include: Improving on-demand strategy annotations;first-order logic as a constraint programming language;maintenance of formal software developments by stratified verification;a note on universal measures for weak implicit computational complexity;extending compositional message sequence graphs;searching for invariants using temporal resolution;proof planning for feature interactions;an extension of BDICTL with functional dependencies and components;directed automated theorem proving;a framework for splitting BDI agents;on the complexity of disjunction and explicit definability properties in some intermediate logics;using BDDs with combinations of theories;on expressive description logics with composition of roles in number restrictions;query optimization of disjunctive databases with constraints through binding propagation;a non-commutative extension of MELL;procedural semantics for fuzzy disjunctive programs;pushdown specifications;theorem proving with sequence variables and flexible arity symbols;parallelism and tree regular constraints;a semantics for proof plans with applications to interactive proof planning;an isomorphism between a fragment of sequent calculus and an extension of natural deduction;a local system for linear logic;investigating type-certifying compilation with isabelle;automating type soundness proofs via decision procedures and guided reductions and abox satisfiability reduced to terminological reasoning in expressive description logics.
Disjunctive logicprogramming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. reasoning with DLP is harder than with normal (boolean OR-free) logic pr...
详细信息
Disjunctive logicprogramming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and reasoning. reasoning with DLP is harder than with normal (boolean OR-free) logic programs, because stable model checking-deciding whether a given model is a stable model of a propositional DLP program-is co-NP-complete, while it is polynomial for normal logic programs. this paper proposes a new transformation Gamma(M) (P), which reduces stable model checking to UNSAT-i.e., to deciding whether a given CNF formula is unsatisfiable. the stability of a model M of a program P thus can be verified by calling a Satisfiability Checker on the CNF formula Gamma(M) (P). the transformation is parsimonious (i.e., no new symbol is added), and efficiently computable, as it runs in logarithmic space (and therefore in polynomial time). Moreover, the size of the generated CNF formula never exceeds the size of the input (and is usually much smaller). We complement this transformation with modular evaluation results, which allow for efficient handling of large real-world reasoning problems. the proposed approach to stable model checking has been implemented in DLV-a state-of-the-art implementation of DLP. A number of experiments and benchmarks have been run using SATZ as Satisfiability checker. the results of the experiments are very positive and confirm the usefulness of our techniques. (C) 2003 Elsevier B.V. All rights reserved.
We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear log...
详细信息
ISBN:
(纸本)3540201017
We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together withthe introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.
Prioritized logic programs (PLPs) have a mechanism of representing priority knowledge in logic programs. the declarative semantics of a PLP is given as preferred answer sets which are used for representing nonmonotoni...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
Prioritized logic programs (PLPs) have a mechanism of representing priority knowledge in logic programs. the declarative semantics of a PLP is given as preferred answer sets which are used for representing nonmonotonic reasoning as well as preference abduction. From the computational viewpoint, however, its implementation issues have little been studied and no sound procedure is known for computing preferred answer sets of PLPs. In this paper, we present a sound and complete procedure to compute all preferred answer sets of a PLP in answer set programming. the procedure is based on a program transformation from a PLP to a logic program and is realized on top of any procedure for answer set programming. the proposed technique also extends PLPs to handle dynamic preference and we address its application to legal reasoning.
For automatic theorem provers it is as important to disprove false conjectures as it is to prove true ones, especially if it is not known ahead of time if a formula is derivable inside a particular inference system. S...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
For automatic theorem provers it is as important to disprove false conjectures as it is to prove true ones, especially if it is not known ahead of time if a formula is derivable inside a particular inference system. Situations of this kind occur frequently in inductive theorem proving systems where failure is a common mode of operation. this paper describes an abstraction mechanism for first-order logic over an arbitrary but fixed term algebra to second-order monadic logic with 0 successor functions. the decidability of second-order monadic logic together with our notion of abstraction yields an elegant criterion that characterizes a subclass of unprovable conjectures.
this paper presents an Arabic Morphological Analyzer and its implementation in clp(FD), a constraint logicprogramming language. the Morphological Analyzer (MA) represents a component of an architecture which can proc...
详细信息
ISBN:
(纸本)3540408037
this paper presents an Arabic Morphological Analyzer and its implementation in clp(FD), a constraint logicprogramming language. the Morphological Analyzer (MA) represents a component of an architecture which can process unrestricted text from a source such as Internet. the morphological analyzer uses a constraint-based model to represent the morphological rules for verbs and nouns, a matching algorithm to isolate the affixes and the root of a given word-form, and a linguistic knowledge base consisting in lists of markers. the morphological rules fall into two categories: the regular morphological rules of the Arabic grammar and the exception rules that represent the language exceptions. clp(FD) is particularly suitable for the implementation of our system thanks to its double reasoning: symbolic reasoning expresses the logic properties of the problem and facilitates the implementation of a the linguistic knowledge base, and heuristics, while constraint satisfaction reasoning on finite domains uses constraint propagation to keep the search space manageable.
Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. they axe also frequently used in practical con...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. they axe also frequently used in practical contexts where some interpreted function symbols are present. In particular, for the verification of pipelined microprocessors, in many cases it suffices to be able to deal with integer offsets, that is, instead of only having ground terms t built over free symbols, all (sub)terms can be of the form t + k for arbitrary integer values k. In this paper we first give a different very simple and clean formulation for the standard congruence closure algorithm which we believe is of interest on itself. It builds on ideas from the abstract algorithms of [Kap97,BT00], but it is easily shown to run in the best known time, O(n log n), like the classical algorithms [DST80,NO80,Sho84]. After that, we show how this algorithm can be smoothly extended to deal with integer offsets without increasing this asymptotic complexity.
We introduce a mathematical model of legal reasoning using an underlying conditional logic semantics, to allow its tractability in some special cases. the main idea is to capture the entailment of legal consequences t...
详细信息
ISBN:
(纸本)1581137478
We introduce a mathematical model of legal reasoning using an underlying conditional logic semantics, to allow its tractability in some special cases. the main idea is to capture the entailment of legal consequences through a model of 0-1 programming. For such task, first we model legal reasoning with Lehmann's Lexicographic semantics and then we translate it to an instance of weighted MAXSAT problem, in order to compute the logical consequences of legal reasoning. Hence, combinatorial optimization algorithms can be used to yield the legal consequences of defeasible reasoning over legal conditional knowledge bases.
暂无评论