| |
|
|
| |
| |
|
Date Reviewed |
|
| |
1 - 5 of 5
reviews
|
|
|
 |
|
|
|
|
An expressively complete linear time temporal logic for Mazurkiewicz traces: an experiment with the shortest-paths algorithms
Thiagarajan P., Walukiewicz I. Information and Computation 179(2): 230-249, 2002. Type: Article
The basic result, due to Kamp, concerning the propositional temporal logic of linear time (LTL) interpreted over sequences is that LTL has the same expressive power as the first order theory of sequences. Unfortunately, using sequences...
|
Jul 10 2003 |
|
|
|
|
|
|
LTL is expressively complete for Mazurkiewicz traces
Diekert V., Gastin P. Journal of Computer and System Sciences 64(2): 396-418, 2002. Type: Article
When dealing with concurrent systems, one possible approach is to reduce them to sequential systems, by considering all linearizations. Then, one can apply techniques and tools developed for sequential systems. Using this approach, how...
|
Jun 23 2003 |
|
|
|
|
|
|
The development of CASC
Pelletier F., Sutcliffe G., Suttner C. AI Communications 15(2): 79-90, 2002. Type: Article
A competition on automated theorem proving (ATP), held during conferences on automated deduction (CADE), is described in this paper....
|
Mar 18 2003 |
|
|
|
|
|
|
Automated theorem proving in software engineering
Schumann J., Springer-Verlag New York, Inc., New York, NY, 2001. 228 pp. Type: Book (9783540679899)
It is obvious that the growing demand for high quality, safety, and security of software systems can be met by rigorous application of formal methods during software design. However, tools for formal methods in general do not provide a...
|
Jun 5 2002 |
|
|
|
|
|
|
Clausal temporal resolution
Fisher M., Dixon C., Peim M. ACM Transactions on Computational Logic 2(1): 12-56, 2001. Type: Article
A clausal resolution method for propositional linear temporal logic is presented. The method, originally proposed by Fisher in 1991 [1], is clausal. It works on formulas transformed to a normal form called separated normal form (SNF), ...
|
Aug 1 2001 |
|
|
|
|
|
| |
|
|
| |
|
|
