Graphical languages are standard in the field of computer programming. Complex software development is best handled by graphically connecting pre-built, fully tested and highly specialized software components, instead...
详细信息
Graphical languages are standard in the field of computer programming. Complex software development is best handled by graphically connecting pre-built, fully tested and highly specialized software components, instead of writing and debugging thousands of lines of code. Modern programming environments include complete libraries of such components. In the field of Programmable logic Controllers (PLCs), this is not the case. PLC programs can be developed using graphical languages, as Ladder Diagrams (LD) or Function Block Diagrams (FBD), but the standard libraries are very limited, so the programmer must develop his own libraries, building software objects from scratch. In this paper, a framework is presented for automatically building complex software modules using based on two key pillars: on the one hand, using object oriented concepts as encapsulation, inheritance and generic programming, and, in the other one, closely following the physical model of the objects used in building electrical control cabinets (ECBs).
the proceedings contain 50 papers. the topics discussed include: independently checkable proofs from decision procedures: issues and progress;Zap: automated theorem proving for software analysis;scaling up: computers ...
详细信息
the proceedings contain 50 papers. the topics discussed include: independently checkable proofs from decision procedures: issues and progress;Zap: automated theorem proving for software analysis;scaling up: computers vs. common sense;a new constraint solver for 3D lattices and its application to the protein folding problem;disjunctive constraint lambda calculi;optimizing the runtime processing of types in polymorphic logicprogramming languages;the four sons of penrose;termination of fair computations in term rewriting;matching with regular constraints;automating coherent logic;regular derivations in basic superposition-based calculi;on the specification on sequent systems;experimental evaluation of classical automata constructions;reasoning about incompletely defined programs;a unified memory model for pointers;pushdown module checking;functional correctness proofs of encryption algorithms;and algebraic intruder deductions.
the logic FO(ID) extends classical first order logic withinductive definitions. this paper studies the satisifiability problem for PC(ID), its propositional fragment. We develop a framework for model generation in th...
详细信息
ISBN:
(纸本)354030553X
the logic FO(ID) extends classical first order logic withinductive definitions. this paper studies the satisifiability problem for PC(ID), its propositional fragment. We develop a framework for model generation in this logic, present an algorithm and prove its correctness. As FO(ID) is an integration of classical logic and logicprogramming, our algorithm integrates techniques from SAT and ASP. We report on a prototype system, called MIDL, experimentally validating our approach.
Defeasible logic is extended to programming languages for cognitive agents with preferences and actions for planning. We define rule-based agent theories that contain preferences and actions, together with inference p...
详细信息
ISBN:
(纸本)354030553X
Defeasible logic is extended to programming languages for cognitive agents with preferences and actions for planning. We define rule-based agent theories that contain preferences and actions, together with inference procedures. We discuss patterns of agent types in this setting. Finally, we illustrate the language by an example of an agent reasoning about web-services.
We propose a characterization of provability in Bl's Pointer logic (PL) that is based on semantic structures called resource graphs. this logic has been defined for reasoning about mutable data structures and resu...
详细信息
ISBN:
(纸本)354030553X
We propose a characterization of provability in Bl's Pointer logic (PL) that is based on semantic structures called resource graphs. this logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.
In [2] Gentzen calculi for intuitionistic logic extended with an existence predicate were introduced. Such logics were first introduced by Dana Scott, who provided a proof system for it in Hilbert style. the logic see...
详细信息
ISBN:
(纸本)354030553X
In [2] Gentzen calculi for intuitionistic logic extended with an existence predicate were introduced. Such logics were first introduced by Dana Scott, who provided a proof system for it in Hilbert style. the logic seems particularly useful in settings where non constant domain Kripke models play a role. In this paper it is proved that these systems have interpolation and the Beth definability property.
Answer Set programming (ASP) has been demonstrated as an effective tool in various application areas, including formal verification. In this paper we present Bounded Model Checking (BMC) of Abstract State Machines (AS...
详细信息
ISBN:
(纸本)354030553X
Answer Set programming (ASP) has been demonstrated as an effective tool in various application areas, including formal verification. In this paper we present Bounded Model Checking (BMC) of Abstract State Machines (ASMs) based on ASP. We show how to succinctly translate an ASM and a temporal property into a logic program and solve the BMC problem for the ASM by computing an answer set for the corresponding program. Experimental results for our method using the answer set solvers SMODELS and CMODELS are also given.
We present efficient Pure Pointer Machine (PPM) algorithms to test for "leftness" in dynamic search trees and related problems. In particular, we show that the problem of testing if a node x is in the leftmo...
详细信息
ISBN:
(纸本)354030553X
We present efficient Pure Pointer Machine (PPM) algorithms to test for "leftness" in dynamic search trees and related problems. In particular, we show that the problem of testing if a node x is in the leftmost branch of the subtree rooted in node y, in a dynamic tree that grows and shrinks at the leaves, can be solved on PPMs in worst-case O((lg lg n)(2)) time per operation in the semi-dynamic case-i.e., all the operations that add leaves to the tree are performed before any other operations-where n is the number of operations that affect the structure of the tree. We also show that the problem can be solved on PPMs in amortized O((lg lg n)(2)) time per operation in the fully dynamic case.
We present tableau calculi for some logics of default reasoning, as defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for preferential and cumulative logics. Our calculi are obtained by introduc...
详细信息
ISBN:
(纸本)354030553X
We present tableau calculi for some logics of default reasoning, as defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for preferential and cumulative logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. Moreover, they give a decision procedure for the respective logics and can be used to establish their complexity.
Recently, linear logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear ...
详细信息
ISBN:
(纸本)354030553X
Recently, linear logic has been used to specify sequent calculus proof systems in such a way that the proof search in linear logic can yield proof search in the specified logic. Furthermore, the meta-theory of linear logic can be used to draw conclusions about the specified sequent calculus. For example, derivability of one proof system from another can be decided by a simple procedure that is implemented via bounded logicprogramming-style search. Also, simple and decidable conditions on the linear logic presentation of inference rules, called homogeneous and coherence, can be used to infer that the initial rules can be restricted to atoms and that cuts can be eliminated. In the present paper we introduce Llinda, a logical framework based on linear logic augmented with inference rules for definition (fixed points) and induction. In this way, the above properties can be proved entirely inside the framework. To further illustrate the power of Llinda, we extend the definition of coherence and provide a new, semi-automated proof of cut-elimination for Girard's logic of Unicity (LU).
暂无评论