96views more  ENTCS 2006»
13 years 7 months ago
Verification of AMBA Using a Combination of Model Checking and Theorem Proving
The Advanced Microcontroller Bus Architecture (AMBA) is an open System-onChip bus protocol for high-performance buses on low-power devices. We demonstrate the combined use of mode...
Hasan Amjad
13 years 8 months ago
LCF-style for Secure Verification Platform based on Multiway Decision Graphs
Abstract. Formal verification of digital systems is achieved, today, using one of two main approaches: states exploration (mainly model checking and equivalence checking) or deduct...
Sa'ed Abed, Otmane Aït Mohamed
13 years 8 months ago
Automated Reasoning in Differential Geometry and Mechanics Using Characteristic Method
This paper reports the study of properties of the curve pairs of the Bertrand types using our automated reasoning program based on Wu's method of mechanical theorem proving fo...
Shang-Ching Chou, Xiao-Shan Gao
13 years 8 months ago
Algorithms for Generation in Lambek Theorem Proving
We discuss algorithms for generation within the Lambek Theorem Proving Framework. Efficient algorithms for generation in this framework take a semantics-driven strategy. This stra...
Erik-Jan van der Linden, Guido Minnen
ACL Anthology
13 years 8 months ago
Lambek Theorem Proving And Feature Unification
CT Feature Unification can be integrated with Lambek Theorem Proving in a simple and straightforward way. Two principles determine all distribution of features in LTP. It is not ne...
Erik-Jan van der Linden
13 years 8 months ago
A Feature-Based Learning Method for Theorem Proving
Automatedreasoning or theorem proving essentially amounts to solving search problems. Despite significant progress in recent years theorem provers still have manyshortcomings. The...
Matthias Fuchs
13 years 8 months ago
Automated Reasoning: Past Story and New Trends
We overview the development of first-order automated reasoning systems starting from their early years. Based on the analysis of current and potential applications of such systems...
Andrei Voronkov
13 years 8 months ago
An Executable Semantics of Object-oriented Models for Simulation and Theorem Proving
This paper presents an executable semantics of OO models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing its underlying heap me...
Kenro Yatake, Takuya Katayama
13 years 9 months ago
History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!
Abstract. In this survey on implicit induction I recollect some memories on the history of implicit induction as it is relevant for future research on computer-assisted theorem pro...
Claus-Peter Wirth
13 years 11 months ago
More About TAS and IsaWin - Tools for Formal Program Development
We present a family of tools for program development and verification, comprising the transformation system TAS and the theorem proving interface IsaWin. Both are based on the theo...
Christoph Lüth, Burkhart Wolff