This decommissioned ERA site remains active temporarily to support our final migration steps to https://ualberta.scholaris.ca, ERA's new home. All new collections and items, including Spring 2025 theses, are at that site. For assistance, please contact erahelp@ualberta.ca.
Search
Skip to Search Results- 1ASG
- 1AST
- 1Automated reasoning
- 1C++
- 1Mizar proof checking environment
- 1Mutilated checkerboard problem
-
A Note on "How to Write a Proof"
1996
Trybulec, Andrzej, Rudnicki, Piotr
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...
-
2003
Rudnicki, Piotr, Hoover, Jim, Hou, Daqing
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...
-
The Mutilated Checkerboard Problem in the Lightweight Set Theory of Mizar
1996
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...
-
1991
Rudnicki, Piotr, Hoover, James
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...