this talk explores the relationship between coherent (aka "geometric") logic and first-order logic FOL, with special reference to the coherence/geometricity required of accessibility conditions in Negri'...
详细信息
ISBN:
(纸本)9783319243122;9783319243115
this talk explores the relationship between coherent (aka "geometric") logic and first-order logic FOL, with special reference to the coherence/geometricity required of accessibility conditions in Negri's work on modal logic (and our work with her on intermediate logic). It has been known to some since the 1970s that every first-order theory has a coherent conservative extension, and weaker versions of this result have been used in association withthe automation of coherent logic;but, it is hard to find the result in the literature. We discuss various proofs of the result, and present a coherentisation algorithm withthe desirable property of being idempotent. An announcement was in [7];details can be found in [8].
In this paper, we investigate the use of high-level action languages for representing and reasoning about ethical responsibility in goal specification domains. First, we present a simplified Event Calculus formulated ...
详细信息
ISBN:
(纸本)9783662488997;9783662488980
In this paper, we investigate the use of high-level action languages for representing and reasoning about ethical responsibility in goal specification domains. First, we present a simplified Event Calculus formulated as a logic program under the stable model semantics in order to represent situations within Answer Set programming. Second, we introduce a model of causality that allows us to use an answer set solver to perform reasoning over the agent's ethical responsibility. We then extend and test this framework against the Trolley Problem and the Doctrine of Double Effect. the overarching aim of the paper is to propose a general and adaptable formal language that may be employed over a variety of ethical scenarios in which the agent's responsibility must be examined and their choices determined. Our fundamental ambition is to displace the burden of moral reasoning from the programmer to the program itself, moving away from current computational ethics that too easily embed moral reasoning within computational engines, thereby feeding atomic answers that fail to truly represent underlying dynamics.
Misuse or loss of web application data can have catastrophic consequences in today's Internet oriented world. Hence, verification of web application data models is of paramount importance. We have developed a fram...
详细信息
ISBN:
(纸本)9781509000258
Misuse or loss of web application data can have catastrophic consequences in today's Internet oriented world. Hence, verification of web application data models is of paramount importance. We have developed a framework for verification of web application data models via translation to First Order logic (FOL), followed by automatedtheorem proving. Due to the undecidability of FOL, this automated approach does not always produce a conclusive answer. In this paper, we investigate the use of many-sorted logic in data model verification in order to improve the effectiveness of this approach. Many-sorted logic allows us to specify type information explicitly, thus lightening the burden of reasoning about type information during theorem proving. Our experiments demonstrate that using many-sorted logic improves the verification performance significantly, and completely eliminates inconclusive results in all cases over 7 real world web applications, down from an 17% inconclusive rate.
the implication problem for the class of embedded dependencies is undecidable. However, this does not imply lackness of a proof procedure as exemplified by the chase algorithm. In this paper we present a complete axio...
详细信息
ISBN:
(数字)9783662488997
ISBN:
(纸本)9783662488997;9783662488980
the implication problem for the class of embedded dependencies is undecidable. However, this does not imply lackness of a proof procedure as exemplified by the chase algorithm. In this paper we present a complete axiomatization of embedded dependencies that is based on the chase and uses inclusion dependencies and implicit existential quantification in the intermediate steps of deductions.
the fashion footwear industry is strongly characterized by hand-crafted fabrication. Companies operating in this field are usually reluctant to employ industrial robots in their facilities, where the integration of au...
详细信息
the fashion footwear industry is strongly characterized by hand-crafted fabrication. Companies operating in this field are usually reluctant to employ industrial robots in their facilities, where the integration of automated solutions is often an element of disruption. It is also still difficult to perform many of the operations involved with industrial robots. the roughing of the uppers of fashion shoes is a typical example: the great inaccuracy in shoe dimensions and shape makes definition of an automated path a critical aspect, and this is reflected in the complexity of robot programming. In addition, standard industrial position-based control solutions are unsuitable in force-tracking application as roughing by the variable stiffness of the environment and by arm flexibilities. In this scenario, the paper describes an innovative robotic cell for roughing operations with a layout conceived for installation in artisan-based production. the robot controller is an admittance control loop with a fuzzy regulator designed to be integrated with standard robot controller by exploiting the so-called sensor-tracking option. the design of the robot controller is grounded on an in-depth analysis of the manual strategies used by workers skilled in roughing operations. the results of a series of experiments on different kinds of shoes demonstrate the feasibility of this approach.
Intrusion Detection System (IDS) is an essential component of the network security infrastructure. It detects malicious activities by monitoring network traffic. there are two main classes of IDS: the anomaly-based ID...
详细信息
ISBN:
(纸本)9781479987849
Intrusion Detection System (IDS) is an essential component of the network security infrastructure. It detects malicious activities by monitoring network traffic. there are two main classes of IDS: the anomaly-based IDS and signature-based IDS. An important challenge, for signature-based IDS, is automating attack signature writing from traffic logs, which can be very hard to be established for human administrator. In this paper, we propose a solution addressing this challenge. We propose cloud-based signature learning service using Inductive logicprogramming (ILP). Learning service generates rule describing properties shared by packets labelled as malicious and that do not cover normal packets. the system uses a background knowledge composed of predicates used to describe network attack signature. the cloud architecture of our IDS enables it to have specialized nodes. Preliminary experimentations show that the proposed system is able to reproduce automatically SNORT signature.
We present Probabilistic Doxastic Temporal (PDT) logic, a formalism to represent and reason about probabilistic beliefs and their evolution in multi-agent systems. It can quantify beliefs through probability intervals...
详细信息
ISBN:
(纸本)9789897580741
We present Probabilistic Doxastic Temporal (PDT) logic, a formalism to represent and reason about probabilistic beliefs and their evolution in multi-agent systems. It can quantify beliefs through probability intervals and incorporates the concepts of frequency functions and epistemic actions. We provide an appropriate semantics for PDT and show how agents can update their beliefs with respect to their observations.
the proceedings contain 42 papers. the special focus in this conference is on automated Deduction. the topics include: History and prospects for first-order automated deduction;stumbling around in the dark: lessons fr...
the proceedings contain 42 papers. the special focus in this conference is on automated Deduction. the topics include: History and prospects for first-order automated deduction;stumbling around in the dark: lessons from everyday mathematics;automatedreasoning in the wild;confluence competition 2015;term rewriting with prefix context constraints and bottom-up strategies;encoding dependency pair techniques and control strategies for maximal completion;reducing relative termination to dependency pair problems;decidability of univariate real algebra with predicates for rational and integer powers;a formalisation of finite automata using hereditarily finite sets;inductive beluga: programming proofs;quantifier-free equational logic and prime implicate generation;quantomatic: a proof assistant for diagrammatic reasoning;cooperating proof attempts;towards the compression of first-order resolution proofs by lowering unit clauses;a polite non-disjoint combination method: theories with bridging functions revisited;exploring theories with a model-finding assistant;abstract interpretation as automated deduction;a uniform substitution calculus for differential dynamic logic;program synthesis using dual interpretation;automatedtheorem proving for assertions in separation logic with all connectives;tableaux methods for propositional dynamic logics with separating parallel composition;regular patterns in second-order unification;theorem proving with bounded rigid e-unification and linear integer arithmetic revisited.
Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of ...
详细信息
ISBN:
(纸本)9783662488997;9783662488980
Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of rules from interfering. In this paper, we propose a module system for a small logically-motivated rule-based language. the resulting modules are nothing more than rewrite rules of a specific form, which are themselves just logic formulas. Yet, they provide some of the same features found in advanced module systems such as that of Standard ML, in particular name space separation, support for abstract data types, and parametrization (functors in ML). Our modules also offer essential features for concurrent programming such as facilities for sharing private names. this approach is directly applicable to other rule-based languages, including most forward-chaining logicprogramming languages and many process algebras.
In linear logic, formulas can be split into two sets: classical (those that can be used as many times as necessary) or linear (those that are consumed and no longer available after being used). Subexponentials general...
详细信息
ISBN:
(数字)9783662488997
ISBN:
(纸本)9783662488997;9783662488980
In linear logic, formulas can be split into two sets: classical (those that can be used as many times as necessary) or linear (those that are consumed and no longer available after being used). Subexponentials generalize this notion by allowing the formulas to be split into many sets, each of which can then be specified to be classical or linear. this flexibility increases its expressiveness: we already have adequate encodings of a number of other proof systems, and for computational models such as concurrent constraint programming, in linear logic with subexponentials (SEL). Bigraphs were proposed by Milner in 2001 as a model for ubiquitous computing, subsuming models of computation such as CCS and the pi-calculus and capable of modeling connectivity and locality at the same time. In this work we present an encoding of the bigraph structure in SEL, thus giving an indication of the expressive power of this logic, and at the same time providing a framework for reasoning and operating on bigraphs. Our encoding is adequate and therefore the operations of composition and juxtaposition can be performed on the logical level. Moreover, all the proof-theoretical tools of SEL become available for querying and proving properties of bigraph structures.
暂无评论