Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipe...
详细信息
ISBN:
(纸本)354030553X
Separation logic is a subset of the quantifier-free first order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipelined processor designs and timed systems, In this paper, we present a fast decision procedure for separation logic, which combines Boolean satisfiability (SAT) with a graph based incremental negative cycle elimination algorithm. Our solver abstracts a separation logic formula into a Boolean formula by replacing each predicate with a Boolean variable. Transitivity constraints over predicates are detected from the constraint graph and added on a need-to basis. Our solver handles Boolean and theory conflicts uniformly at the Boolean level. the graph based algorithm supports not only incremental theory propagation, but also constant time theory backtracking without using a cumbersome history stack. Experimental results on a large set of benchmarks show that our new decision procedure is scalable, and outperforms existing techniques for this logic.
First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and ...
详细信息
ISBN:
(纸本)354030553X
First-order coherent logic (CL) extends resolution logic in that coherent formulas allow certain existential quantifications. A substantial number of reasoning problems (e.g., in confluence theory, lattice theory and projective geometry) can be formulated directly in CL without any clausification or Skolemization. CL has a natural proof theory, reasoning is constructive and proof objects can easily be obtained. We prove completeness of the proof theory and give a linear translation from FOL to CL that preserves logical equivalence. these properties make CL well-suited for providing automated reasoning support to logical frameworks. the proof theory has been implemented in Prolog, generating proof objects that can be verified directly in the proof assistant Coq. the prototype has been tested on the proof of Hessenberg's theorem, which could be automated to a considerable extent. Finally, we compare the prototype to some automated theorem provers on selected problems.
the main goal of this paper is to apply rewriting termination technology-enjoying a quite mature set of termination results and tools-to the problem of proving automatically the termination of concurrent systems under...
详细信息
ISBN:
(纸本)354030553X
the main goal of this paper is to apply rewriting termination technology-enjoying a quite mature set of termination results and tools-to the problem of proving automatically the termination of concurrent systems under fairness assumptions. We adopt the thesis that a concurrent system can be naturally modeled as a rewrite system, and develop a reductionistic theoretical approach to systematically transform, under reasonable assumptions, fair-termination problems into ordinary termination problems of associated relations, to which standard rewriting termination techniques and tools can be applied. Our theoretical results are combined into a practical proof methodology for proving fair-termination that can be automated and can be supported by current termination tools. We illustrate this methodology with some concrete examples and briefly comment on future extensions.
the traditional purpose of types in programming languages of providing correctness assurances at compile time is increasingly being supplemented by a direct role for them in the computational process. In the context o...
详细信息
ISBN:
(纸本)354030553X
the traditional purpose of types in programming languages of providing correctness assurances at compile time is increasingly being supplemented by a direct role for them in the computational process. In the context of typed logicprogramming, this is manifest in their effect on the unification operation. their influence takes two different forms. First, in a situation where polymorphism is permitted, type information is needed to determine if different occurrences of the same name in fact denote an identical constant. Second, type information may determine the form of bindings for variables. When types are needed for the second purpose as in the case of higher-order unification, these have to be available with every variable and constant. However, in situations such as first-order and higher-order pattern unification, types have no impact on the variable binding process. As a consequence, type examination is needed in these situations only for the first of the two purposes described and even here a careful preprocessing can considerably reduce their run-time footprint. We develop a scheme for treating types in these contexts that exploits this observation. Under this scheme, type information is elided in most cases and is embedded into term structure when this is not entirely possible. Our approach obviates types when properties known as definitional genericity and type preservation are satisfied and has the advantage of working even when these conditions are violated.
the notion of comparative similarity 'X is more similar or closer to Y than to Z' has been investigated in both foundational and applied areas of knowledge representation and reasoning, e.g., in concept format...
详细信息
ISBN:
(纸本)354030553X
the notion of comparative similarity 'X is more similar or closer to Y than to Z' has been investigated in both foundational and applied areas of knowledge representation and reasoning, e.g., in concept formation, similarity- based reasoning and areas of bioinformatics such as protein sequence alignment. In this paper we analyse the computational behaviour of the 'propositional' logic withthe binary operator 'closer to a set tau(1) than to a set tau(2)' and nominals interpreted over various classes of distance (or similarity) spaces. In particular, using a reduction to the emptiness problem for certain tree automata, we show that the satisfiability problem for this logic is ExpTime- complete for the classes of all finite symmetric and all finite (possibly non-symmetric) distance spaces. For finite subspaces of the real line (and higher dimensional Euclidean spaces) we prove the undecidability of satisfiability by a reduction of the solvability problem for Diophantine equations. As our closer' operator has the same expressive power as the standard operator > of conditional logic, these results may have interesting implications for conditional logic as well.
We consider automated reasoning about recursive partial functions with decidable domain, i.e. functions computed by incompletely defined but terminating functional programs. Incomplete definitions provide an elegant a...
详细信息
ISBN:
(纸本)354030553X
We consider automated reasoning about recursive partial functions with decidable domain, i.e. functions computed by incompletely defined but terminating functional programs. Incomplete definitions provide an elegant and easy way to write and to reason about programs which may halt with a run time error by throwing an exception or printing an error message, e.g. when attempting to divide by zero. We investigate the semantics of incompletely defined programs, define an interpreter for those programs and discuss the termination of incompletely defined procedures. We then analyze which problems need to be solved if a theorem prover designed for verification of completely defined programs is modified to work for incompletely defined programs as well. We also discuss how to reason about stuck computations which arise when calling incompletely defined procedures with invalid arguments. Our method of automated reasoning about incompletely defined programs has been implemented in the verification tool VeriFun. We conclude by discussing experiences obtained in several case studies withthis implementation and also compare and relate our proposal to other work.
Simulation-based study plays important roles in robotic systems development. this paper describes robot-in-the-loop simulation, which is a novel simulation method that we developed to allow real robots and robot model...
详细信息
Simulation-based study plays important roles in robotic systems development. this paper describes robot-in-the-loop simulation, which is a novel simulation method that we developed to allow real robots and robot models to work together for system-wide measurement and test. To support robot-in-the-loop simulation, a simulated virtual environment is developed. Several kinds of sensor/actuator interface models are defined to allow real robots to interact withthe virtual environment. To demonstrate the capability of robot-in-the-loop simulation, three mobile robot examples were developed and are presented in the paper in an incremental way. these examples illustrate the usages and configurations of robot-in-the-loop simulation under different situations
the types of learning systems used in the description language and its related domains are investigated. these learning systems are able to exploit meta-information to improve their performance. An algorithm, which au...
详细信息
the types of learning systems used in the description language and its related domains are investigated. these learning systems are able to exploit meta-information to improve their performance. An algorithm, which automatically identifies types from types is proposed. the performance of the algorithm in domains with different characteristics, and its robustness with respect to incomplete observations are studied.
Aspect-oriented software development (AOSD) techniques support systematic modularization and composition of crosscutting concerns. though AOSD techniques have been proposed to handle crosscutting concerns at various s...
详细信息
Aspect-oriented software development (AOSD) techniques support systematic modularization and composition of crosscutting concerns. though AOSD techniques have been proposed to handle crosscutting concerns at various stages during the software life cycle, there is a traceability gap between the aspects at the requirements level and those at later development stages. It is not clear what proof obligations about an aspect-oriented implementation follow from the initial aspectual requirements. this work presents PROBE, a framework for generation of proof obligations for aspect-oriented systems from the initial aspectual requirements and associated trade-offs. the abstract proof obligations are expressed in standard linear temporal logic. Key components of the framework include an extended ontology with parametric temporal formulas and functions, and extensive treatment of conflicts among requirements. the resultant temporal logic assertions, grouped into specifications of aspect implementations, can then be instantiated in terms of the implementation and verification tools.
this paper presents a method for detecting the connecting points in connected thai printed characters. In thai Optical Character Recognition systems, an important problem that decreases the accuracy is the connected c...
详细信息
ISBN:
(纸本)0769519482
this paper presents a method for detecting the connecting points in connected thai printed characters. In thai Optical Character Recognition systems, an important problem that decreases the accuracy is the connected characters. these characters could cause the errors in segmentation process. To attack this problem, we first extract the features of the connecting points in the character images. then, we employ inductivelogicprogramming to produce the rules that will be used to classify the unseen images. Finally, we use a Backpropagation Neural Network to make these rules more flexible. the experimental results show that our method achieves 94.94% accuracy.
暂无评论