SearchSkip to Search Results
A Note on "How to Write a Proof"
Technical report TR96-08. We believe that mechanical checking of real-life proofs can become practical and therefore we use Mizar---a proof checking system for proofs written in a style of traditional mathematics. In the beginning of 1994 we came across a copy of L. Lamport's paper in which \"a...
Introduction: Some problems that are difficult for automated theorem provers (ATPs) are so merely because of their size, but not because of any logical or conceptual complexity. Examples of this type of difficult problem have been published in the past: see Pelletier [1986: problems 12, 29, 34,...
The Mutilated Checkerboard Problem in the Lightweight Set Theory of Mizar
Technical report TR96-09. An 8 by 8 checkerboard with two diagonally opposite squares removed cannot be covered by 2 by 1 dominoes. John McCarthy postulates that a mechanized system of heavy duty set theory should accept his formal description of the proposition and his proof that the covering...
Technical report TR91-02. We present a very simple protocol for the self-stabilizing orientation of a unicyclic network of uniform processors. It has the same O(n2) performance as the Israeli and Jalfon protocol for rings but is much simpler to state and furthermore operates under the weaker...
Technical report TR03-22. Different program analyses require different information from the source code. For some applications, an AST (Abstract Syntax Tree) representation of the source may be sufficient. We want to be able to specify assertions on the structure of a program without mentioning...