Currently displaying 1 – 11 of 11

Showing per page

Order by Relevance | Title | Year of publication

Countable Toronto spaces

Gary GruenhageJ. Moore — 2000

Fundamenta Mathematicae

A space X is called an α-Toronto space if X is scattered of Cantor-Bendixson rank α and is homeomorphic to each of its subspaces of the same rank. We answer a question of Steprāns by constructing a countable α-Toronto space for each α ≤ ω. We also construct consistent examples of countable α-Toronto spaces for each α < ω 1 .

Some key research problems in automated theorem proving for hardware and software verification.

Matt KaufmannJ. Strother Moore — 2004

RACSAM

This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition,...

Page 1

Download Results (CSV)