We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint logic. this logic is capable of expressing many interesting properties which are not regular and, hence, not expressibl...
详细信息
ISBN:
(纸本)9783540755586
We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint logic. this logic is capable of expressing many interesting properties which are not regular and, hence, not expressible in the modal mu-calculus. the algorithm avoids best-case exponential behaviour by localising the computation of functions and can be implemented symbolically using BDDs. We show how insight into the behaviour of this procedure, when run on a fixed formula, can be used to obtain specialised algorithms for particular problems. this yields, for example, the competitive antichain algorithm for NFA universality but also a new algorithm for a string matching problem.
In this paper we discuss the new version of PITP, a procedure to decide propositional intuitionistic logic, which turns out at the moment to be the best propositional prover on ILTP. the changes in the strategy and im...
详细信息
ISBN:
(纸本)9783540730989
In this paper we discuss the new version of PITP, a procedure to decide propositional intuitionistic logic, which turns out at the moment to be the best propositional prover on ILTP. the changes in the strategy and implementation make the new version of PITP faster and capable of deciding more formulas than the previous one. We give a short account both of the old optimizations and the changes in the strategy with respect to the previous version. We use ILTP library and random generated formulas to compare the implementation described in this paper to the other provers (including our old version of PITP).
We study logic programs with arbitrary abstract constraint atoms, called c-atoms. As a theoretical means to analyze program properties, we investigate the possibility of unfolding these programs to logic programs comp...
详细信息
ISBN:
(纸本)9783540721994
We study logic programs with arbitrary abstract constraint atoms, called c-atoms. As a theoretical means to analyze program properties, we investigate the possibility of unfolding these programs to logic programs composed of ordinary atoms. this approach reveals some structural properties of a program with c-atoms, and enables characterization of these properties based on the known properties of the transformed program. Furthermore, this approach leads to a straightforward definition of answer sets for disjunctive programs with c-atoms, where a c-atom may appear in the head of a rule as well as in the body. We also study the complexities for various classes of logic programs with c-atoms.
Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But ...
详细信息
ISBN:
(纸本)9783540730989
Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent "cut-free" sequent calculus for BiInt has recently been shown by Uustalu to fail cut-elimination. We present a new cut-free sequent calculus for BiInt, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between implication and its dual, similarly to future and past modalities in tense logic. Our calculus handles this interaction using extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of failed derivation trees. Our simple termination argument allows our calculus to be used for automated deduction, although this is not its main purpose.
the proceedings contain 19 papers. the topics discussed include: nonmonotonic description logics-requirements, theory, and implementations;our quest for the holy grail of agent verification;an abstract framework for s...
详细信息
ISBN:
(纸本)9783540730989
the proceedings contain 19 papers. the topics discussed include: nonmonotonic description logics-requirements, theory, and implementations;our quest for the holy grail of agent verification;an abstract framework for satisfiability modulo theories;axiom pinpointing in general tableaux;proof theory for first order Lukasiewicz logic;a tableau method for public announcement logics;bounded model checking with description logicreasoning;tableau systems for logics of subinterval structures over dense orderings;a cut-free sequent calculus for bi-intuitionistic logic;tableaux with dynamic filtration for layered modal logics;the neighbourhood of S0.9 and S1;EXPTIME tableaux with global caching for description logics with transition roles, inverse roles and role hierarchies;and tree-sequent methods for subintuitionistic predicate logics.
Most complete SAT/ASP solvers are based on DPLL. One of the constraint propagation methods is the so-called lookahead, which has been somewhat controversial, due to its high overhead. In this paper, we show characteri...
详细信息
ISBN:
(纸本)9783540721994
Most complete SAT/ASP solvers are based on DPLL. One of the constraint propagation methods is the so-called lookahead, which has been somewhat controversial, due to its high overhead. In this paper, we show characterizations of the problems for which lookahead is ineffective, and demonstrate, experimentally, that for problems that lie in the phase transition regions, search efficiency can be improved significantly by lookahead. this understanding leads to the proposal of a mechanism called adaptive lookahead, which decides when lookahead should be invoked dynamically upon learned information. Our experiments show that adaptive lookahead adapts well to different situations where lookahead may or may not be beneficial.
We present a framework for updating logic programs under the answer-set semantics that builds on existing work on preferences in logicprogramming. the approach is simple and general, making use of two distinct comple...
详细信息
ISBN:
(纸本)9783540721994
We present a framework for updating logic programs under the answer-set semantics that builds on existing work on preferences in logicprogramming. the approach is simple and general, making use of two distinct complementary techniques: defaultification and preference. While defaultification resolves potential conflicts by inducing more answer sets, preferences then select among these answer sets, yielding the answer sets generated by those rules that have been added more recently. We examine instances of the framework with respect to various desirable properties;for the most part, these properties are satisfied by instances of our framework. Finally, the proposed framework is also easily implementable by off-the-shelf systems.
Two sets of rules are said to be strongly equivalent to each other if replacing one by the other within any logic program preserves the program's stable models. the familiar characterization of strong equivalence ...
详细信息
ISBN:
(纸本)9783540721994
Two sets of rules are said to be strongly equivalent to each other if replacing one by the other within any logic program preserves the program's stable models. the familiar characterization of strong equivalence of grounded programs in terms of the propositional logic of here-and-there is extended in this paper to a large class of logic programs with variables. this class includes, in particular, programs with conditional literals and cardinality constraints. the first-order version of the logic of here-and-there required for this purpose involves two additional non-intuitionistic axiom schemas.
Recent work in network security has focused on the fact that combinations of exploits are the typical means by which an attacker breaks into a network. Researchers have proposed a variety of graph-based analysis appro...
详细信息
ISBN:
(纸本)9780769529837
Recent work in network security has focused on the fact that combinations of exploits are the typical means by which an attacker breaks into a network. Researchers have proposed a variety of graph-based analysis approach, and there is often a lack of logical formalism. this paper describes a new approach to represent and analyze network vulnerability. We propose logical exploitation graph, which directly illustrate logical dependencies among exploitation goals and network configure. Our logical exploitation graph generation tool builds upon LEG-NSA, a network security analyzer based on Prolog logical programming. We demonstrate how to reason all exploitation paths using bottom-up and top-down evaluation algorithms in the Prolog logic-programming engine. We show experimental evidence that our logical exploitation graph generation algorithm is very efficient.
Error back-propagation-and its many variations-has been used extensively to train neural networks. A multi-lager system cannot be trained in a supervised learning scheme because data are usually provided only as end-t...
详细信息
ISBN:
(纸本)0769530508
Error back-propagation-and its many variations-has been used extensively to train neural networks. A multi-lager system cannot be trained in a supervised learning scheme because data are usually provided only as end-to-end input-output pairs for the global system. the central idea of error back-propagation is to derive target input-output pairs for each layer in the system from the global input-output data. We propose a new;method for error-back propagation in a fuzzy Description logicreasoning system. this permits us to derive input-output data pairs in a two-layer setup for training the lower-layer classifiers. To the best of our knowledge, this is the first error back-propagation method for a logicreasoning system.
暂无评论