We present a system of first order logic, together with soundness and completeness proofs wrt. standard first order semantics. Proofs are mechanised in Isabelle/HOL. Our definitions are computable, allowing us to deri...
详细信息
ISBN:
(纸本)3540283722
We present a system of first order logic, together with soundness and completeness proofs wrt. standard first order semantics. Proofs are mechanised in Isabelle/HOL. Our definitions are computable, allowing us to derive an algorithm to test for first order validity. this algorithm may be executed in Isabelle/HOL using the rewrite engine. Alternatively the algorithm has been ported to OCaML.
In Ubiquitous computing small embedded sensor and computing nodes are one of the main enabling technologies. System programming for such small embedded systems is a challenging task involving various hardware componen...
详细信息
ISBN:
(纸本)3540252738
In Ubiquitous computing small embedded sensor and computing nodes are one of the main enabling technologies. System programming for such small embedded systems is a challenging task involving various hardware components with different characteristics. this paper presents a file system for sensor nodes platforms providing a common organization structure and a lightweight and uniform access model for sensors and all other resources on sensor nodes. this mechanism forms an abstraction from different hardware, makes functions re-useable and simplifies the development on such systems. With ParticleFS an file system implementation on a sensor node platform is shown. As an example a telnet application running on sensor nodes was implemented demonstrating the usage of the approach for system programming on such platforms.
Several tools exist for reasoning about JAVA programs annotated with JML specifications. A main issue is to deal with possible aliasing between objects and to handle correctly the frame conditions limiting the part of...
详细信息
ISBN:
(纸本)3540283722
Several tools exist for reasoning about JAVA programs annotated with JML specifications. A main issue is to deal with possible aliasing between objects and to handle correctly the frame conditions limiting the part of memory that a method is allowed to modify. Tools designed for automatic use (like ESC/JAvA) are not complete and even not necessarily correct. On the other side, tools which offer a full modeling of the program require a heavy user interaction for discharging proof obligations. In this paper, we present the modeling of JAVA programs used in the KRAKATOA tool, which generates proof obligations expressed in a logic language suitable for both automatic and interactive reasoning. Using the SIMPLIFY automatic theorem prover, we are able to establish automatically more properties than static analysis tools, with a method which is guaranteed to be sound, assuming only the correctness of our logical interpretation of programs and specifications.
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.
A major technique to address state explosion problem in model checking is abstraction. Predicate abstraction has been applied successfully to large software and now to hardware descriptions, such as Verilog. this pape...
详细信息
ISBN:
(纸本)3540298967
A major technique to address state explosion problem in model checking is abstraction. Predicate abstraction has been applied successfully to large software and now to hardware descriptions, such as Verilog. this paper evaluates the state-of-the-art AI techniques-constraint logicprogramming (CLP)-to improve the performance of predication abstraction of hardware designs, and compared it withthe SAT-based predicate abstraction techniques. With CLP based techniques, we can model various constraints, such as bit, bit-vector and integer, in a uniform framework;we can also model the word-level constraints without flatting them into bit-level constraints as SAT-based method does. Withthese advantages, the computation of abstraction system can be more efficient than SAT-based techniques. We have implemented this method, and the experimental results have shown the promising improvements on the performance of predicate abstraction of hardware designs.
In this study we investigate an inter-industrial and inter-regional recycling system for industrial waste by the cement industry in Japan. We develop a linear programming model that represents cement production proces...
详细信息
ISBN:
(纸本)8251920418
In this study we investigate an inter-industrial and inter-regional recycling system for industrial waste by the cement industry in Japan. We develop a linear programming model that represents cement production processes and waste transportation of all cement factories in Japan. We assess inter-regional material flows of industrial waste, and environmental effects of recycling.
this paper presents an efficient test solution for VLSI circuits. the test structure is designed with GF(2p) CA. the introduction to an innovative scheme of logic folding optimizes the cost of test logicthat can not ...
详细信息
Linear programming is a basic mathematical technique for optimizing a linear function on a domain that is constrained by linear inequalities. We restrict ourselves to linear programs on bounded domains that involve on...
详细信息
ISBN:
(纸本)3540283722
Linear programming is a basic mathematical technique for optimizing a linear function on a domain that is constrained by linear inequalities. We restrict ourselves to linear programs on bounded domains that involve only real variables. In the context of theorem proving, this restriction makes it possible for any given linear program to obtain certificates from external linear programming tools that help to prove arbitrarily precise bounds for the given linear program. To this end, an explicit formalization of matrices in Isabelle/HOL is presented, and how the concept of lattice-ordered rings allows for a smooth integration of matrices withthe axiomatic type classes of Isabelle. As our work is a contribution to the Flyspeck project, we argue that withthe above techniques it is now possible to prove bounds for the linear programs arising in the proof of the Kepler conjecture sufficiently fast.
Tuple centres allow for dynamic programming of the coordination media: coordination laws are expressed and enforced as the behaviour specification of tuple centres, and can change over time. Since time is essential in...
详细信息
ISBN:
(纸本)354025630X
Tuple centres allow for dynamic programming of the coordination media: coordination laws are expressed and enforced as the behaviour specification of tuple centres, and can change over time. Since time is essential in a large number of coordination problems and patterns (involving timeouts, obligations, commitments), coordination laws should be expressive enough to capture and govern time-related issues. Along this line, in this paper we discuss how tuple centres and the ReSpecT language for programminglogic tuple centres can be extended to catch with time, and to support the definition and enforcement of time-aware coordination policies. Some examples are provided to demonstrate the expressiveness of the ReSpecT language to model timed coordination primitives and laws.
"Forsoksgymnaset in Oslo" was an experiment in School Democracy that started classes in automatic data processing in the fall of 1968 as a part of school mathematics in the 11(th) year. We started simple pro...
详细信息
ISBN:
(纸本)0387241671
"Forsoksgymnaset in Oslo" was an experiment in School Democracy that started classes in automatic data processing in the fall of 1968 as a part of school mathematics in the 11(th) year. We started simple programming in FORTRAN on punched cards, off line. Later we had a teletype terminal with paper tape, changed to the BASIC language, and ran programs online by telephone to a distant computer. We also designed the logic simulator "Benjamin", with four "And", "Or", and "Not" elements, battery and lamps, which could be connected in logical networks to be studied. In 1970, we arranged two two-day seminars for teachers during the Christmas and the summer holidays and presented the whole course. We did this eight times and helped to qualify many teachers. the first Examen Artium in Data was organised in June 1970.
暂无评论