Search

We present a symbolic definition that captures some cases of election verifiability for electronic voting protocols. Our definition is given in terms of reachability assertions in the applied pi calculus and is amenable to automated reasoning using the software tool ProVerif. The definition distinguishes three aspects of verifiability, which we call individual, universal, and eligibility verifiability. We demonstrate the applicability of our formalism by analysing the protocols due to Fujioka, Okamoto & Ohta and a variant of the one by Juels, Catalano & Jakobsson (implemented as Civitas by Clarkson, Chong & Myers). [ABSTRACT FROM AUTHOR]

Ordered resolution and superposition are the state-of-the-art proof procedures used in saturation-based theorem proving, for non equational and equational clause sets respectively. In this paper, we present extensions of these calculi that permit one to reason about formulae built from terms with integer exponents (or I-terms), a schematisation language allowing one to denote infinite sequences of iterated terms [8]. We prove that the ordered resolution calculus is still refutationally complete when applied on (non equational) clauses containing I-terms. In the equational case, we prove that the superposition calculus is not complete in the presence of I-terms and we devise a new inference rule, called H-superposition, that restores completeness. [ABSTRACT FROM AUTHOR]

A syllogism, also known as a rule of inference, is a formal logical scheme used to draw a conclusion from a set of premises. In a categorical syllogisms, every premise and conclusion is given in form a of quantified relationship between two objects. The syllogistic system consists of systematically combined premises and conclusions to so called figures and moods. The syllogistic system is a theory for reasoning, developed by Aristotle, who is known as one of the most important contributors of the western thought and logic. Since Aristotle, philosophers and sociologists have successfully modelled human thought and reasoning with syllogistic structures. However, a major lack was that the mathematical properties of the whole syllogistic system could not be fully revealed by now. To be able to calculate any syllogistic property exactly, by using a single algorithm, could indeed facilitate modelling possibly any sort of consistent, inconsistent or approximate human reasoning. In this paper we present such an algorithm. [ABSTRACT FROM AUTHOR]

Recently server consolidation using virtualization leverages cloud computing. In cloud computing, we can apply centralized logging system using server consolidation. In this paper we propose a log analysis method in cloud computing environment using automated reasoning. On cloud computing providers, VM (virtual machine) monitoring is important to detect security incident. We discuss how to monitor VM, formatting and analyzing logs. Automated reasoning is more effective to retrieves information from large amount of log string. In proposed system, VM log is represented as clausal form and processed by FoL (First order Logic) theorem prover. We also present the numerical output of proposed system. [ABSTRACT FROM AUTHOR]

A categorical syllogism is a rule of inference, consisting of two premisses and one conclusion. Every premiss and conclusion consists of dual relationships between the objects M, P, S. Logicians usually use only true syllogisms for deductive reasoning. After predicate logic had superseded syllogisms in the 19th century, interest on the syllogistic system vanished. We have analysed the syllogistic system, which consists of 256 syllogistic moods in total, algorithmically. We have discovered that the symmetric structure of syllogistic figure formation is inherited to the moods and their truth values, making the syllogistic system an inherently symmetric reasoning mechanism, consisting of 25 true, 100 unlikely, 6 uncertain, 100 likely and 25 false moods. In this contribution, we discuss the most significant statistical properties of the syllogistic system and define on top of that the fuzzy syllogistic system. The fuzzy syllogistic system allows for syllogistic approximate reasoning inductively learned M, P, S relationships. [ABSTRACT FROM AUTHOR]

Based on sliding-window rule application and extraction filtering, we present a framework for extracting multi-slot frames describing chemical reactions from Thai free text with unknown target-phrase boundaries. A supervised rule learning algorithm is employed for automatic construction of pattern-based extraction rules from hand-tagged training phrases. A filtering method is devised for removal of incorrect extraction results based on features observed from text portions appearing between adjacent slot fillers in source documents. Extracted reaction frames are represented as concept expressions in description logics and are used as metadata for document indexing. A document knowledge base supporting semantics-based information retrieval is constructed by integrating document metadata with domain-specific ontologies. [ABSTRACT FROM AUTHOR]

Ranking and optimization of web service compositions are some of the most interesting challenges at present. Since web services can be enhanced with formal semantic descriptions, forming the ˵semantic web services″, it becomes conceivable to exploit the quality of semantic links between services (of any composition) as one of the optimization criteria. For this we propose to use the semantic similarities between output and input parameters of web services. Coupling this with other criteria such as quality of service (QoS) allow us to rank and optimize compositions achieving the same goal. Here we suggest an innovative and extensible optimization model designed to balance semantic fit (or functional quality) with non-functional QoS metrics. To allow the use of this model in the context of a large number of services as foreseen by the strategic EC-funded project SOA4All we propose and test the use of Genetic Algorithms. [ABSTRACT FROM AUTHOR]

When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem provers, in contrast, present proofs usually at a fixed level of detail (also called granularity). Often these presentations are neither intended nor suitable for human use. A challenge therefore is to develop user- and goal-adaptive proof presentation techniques that obey common mathematical practice. We present a flexible and adaptive approach to proof presentation based on classification. Expert knowledge for the classification task can be hand-authored or extracted from annotated proof examples via machine learning techniques. The obtained models are employed for the automated generation of further proofs at an adapted level of granularity. [ABSTRACT FROM AUTHOR]

Euler diagrams have been used for centuries as a means for conveying logical statements in a simple, intuitive way. They form the basis of many diagrammatic notations used to represent set-theoretic relationships in a wide range of contexts including software modelling, logical reasoning systems, statistical data representation, database search queries and file system management. In this paper we consider some notations based on Euler diagrams, in particular Spider Diagrams and Constraint Diagrams, with particular emphasis on the development of reasoning systems. [ABSTRACT FROM AUTHOR]

During the process of constructing data mining metadata, the evolution of data mining techniques, the different experiences and views of related organizations inevitably cause inconsistencies. However, current data mining metadata lacks precise semantic due to their description with natural language and graphs, so the automatic consistency checking upon them has not been resolved well. In this paper, a formal logic DLR ]> in the description logic family is proposed. Subsequently, a formal reasoning method based on DLR ]> is designed to automatically check the consistency of data mining metadata. With the description logic DLR ]> , formalization upon the metamodel and metadata of data mining is analyzed in detail. The reasoning engine Racer is applied into the method to check the consistency upon the data mining metadata. Results on the RacerPro reasoning system indicate the method is encouraging. [ABSTRACT FROM AUTHOR]

Automated composition of Web services or the process of forming new value added Web services is one of the most promising challenges in the semantic Web service research area. Semantics is one of the key elements for the automated composition of Web services because such a process requires rich machine-understandable descriptions of services that can be shared. Semantics enables Web service to describe their capabilities and processes, nevertheless there is still some work to be done. Indeed Web services described at functional level need a formal context to perform the automated composition of Web services. The suggested model (i.e., Causal link matrix) is a necessary starting point to apply problem-solving techniques such as regression-based search for Web service composition. The model supports a semantic context in order to find a correct, complete, consistent and optimal plan as a solution. In this paper an innovative and formal model for an AI planning-oriented composition is presented. [ABSTRACT FROM AUTHOR]

This paper generalises the tree-based data structure of ∆-tree to be applied to signed propositional formulas. The ∆-trees allow a compact representation for signed formulas as well as for a number of reduction strategies in order to consider only those occurrences of literals which are relevant for the satisfiability of the input formula. The conversions from signed formulas to ∆- trees and vice versa are described and a notion of restricted form based on this representation is introduced, allowing for a compact representation of formulas in order to consider only those occurrences of literals which are relevant for its satisfiability. [ABSTRACT FROM AUTHOR]