Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more tradi...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures. After an introduction to electronic voting, we describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.
LODE is a logic-based web tool for Italian deaf children. It aims at stimulating global reasoning on e-stories written in a verbal language. Presently, we are focusing on temporal reasoning, that is, LODE stimulates c...
详细信息
ISBN:
(纸本)9783540749691
LODE is a logic-based web tool for Italian deaf children. It aims at stimulating global reasoning on e-stories written in a verbal language. Presently, we are focusing on temporal reasoning, that is, LODE stimulates children to reason with global temporal relations between events possibly distant in a story. this is done through apt exercises and withthe support of a constraint programming system. Children can also reinvent the e-story by rearranging its events along a new temporal order;it is the task of the constraint system to determine the consistency of the temporally reorganised story and provide children with feedback. To the best of our knowledge, LODE is the first e-learning tool for Italian deaf children that aims at stimulating global reasoning on whole e-stories.
Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practica...
详细信息
ISBN:
(纸本)9783540894384
Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practical purposes. In this paper we propose a novel calculus for a large fragment of first-order logic modulo Linear Integer Arithmetic (LIA) that overcomes several limitations of existing theory reasoning approaches. the new calculus - based on the Model Evolution calculus, a first-order logic version of the propositional DPLL procedure - supports restricted quantifiers, requires only a decision procedure for LIA-validity instead of a complete LIA-unification procedure, and is amenable to strong redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete.
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.
the problem of automatedtheorem finding is one of 33 basic research problems in automatedreasoning which was originally proposed by Wos. the problem is still an open problem until now. To solve the problem, a system...
详细信息
ISBN:
(纸本)9783662474877;9783662474860
the problem of automatedtheorem finding is one of 33 basic research problems in automatedreasoning which was originally proposed by Wos. the problem is still an open problem until now. To solve the problem, a systematic methodology with forward reasoning based on strong relevant logic has been proposed. this paper presents a case study of automatedtheorem finding in graph theory to show the generality of the methodology, and presents a future direction for automatedtheorem finding based on the methodology.
Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translat...
详细信息
ISBN:
(纸本)9783540730989
Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translated into a CNF formula. A SAT solver is then applied to the CNF formula, to find a satisfying assignment. Such a satisfying assignment, if found, demonstrates an error in the model of the concurrent system. Description logic (DL) is a family of knowledge representation formalisms, for which reasoning is based on tableaux techniques. We show how Description logic can serve as a natural setting for representing and solving a BMC problem. We formulate a bounded model checking problem as a consistency problem in the DL dialect ACCI. Our formulation results in a compact representation of the model, one that is linear in the size of the model description, and does not involve any unfolding of the model. Experimental results, using the DL reasoner FaCT(++), significantly improve on a previous approach that used DL reasoning for model checking.
We define logic programs with defaults and argumentation theories, a new framework that unifies most of the earlier proposals for defeasible reasoning in logicprogramming. We present a model-theoretic semantics and s...
详细信息
ISBN:
(纸本)9783642028458
We define logic programs with defaults and argumentation theories, a new framework that unifies most of the earlier proposals for defeasible reasoning in logicprogramming. We present a model-theoretic semantics and study its reducibility and well-behavior properties. We use the framework as air elegant and flexible foundation to extend and improve upon Generalized Courteous logic Programs (GCLP) [19]-one of the popular forms of defeasible reasoning. the extensions include higher-order and object-oriented features of Hilog and F-logic [7,21]. the improvements include much simpler, incremental reasoning algorithms and more intuitive behavior. the framework and its Courteous family instantiation were implemented as art extension to the FLORA-2 system.
By using the methods of triple-I reasoning for all implication, we give the solutions of generalized MP rules and MT rules in attribute logic, and propose some approximate reasoning methods based on generalized MP rul...
详细信息
this paper presents a software module for working with fuzzy logic inference systems in the context of fuzzy case-based reasoning. Fuzzy logic, providing tools for describing and handling uncertainty, is an important ...
详细信息
We introduce the probabilistic Description logic. In, axioms are required to hold only in an associated context. the probabilistic component of the logic is given by a Bayesian network that describes the joint probabi...
详细信息
暂无评论