We prove a finite model theorem and infinitary completeness result for the propositional -calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.

Recently, two apparently quite different duality-based approaches to automata minimisation have appeared. One is based on ideas that originated from the controllability-observability duality from systems theory, and the other is based on ideas derived from Stone-type dualities specifically linking coalgebras with algebraic structures derived from modal logics. In the present paper, we develop a more abstract view and unify the two approaches. We show that dualities, or more generally dual adjunctions, between categories can be lifted to dual adjunctions between categories (...) of coalgebras and algebras, and from there to automata with initial as well as final states. As in the Stone-duality approach, algebras are essentially logics for reasoning about the automata. By exploiting the ability to pass between these categories, we show that one can minimize the corresponding automata. We give an abstract minimisation algorithm that has several instances, including the celebrated Brzozowski minimisation algorithm. We further develop three examples that have been treated in previous works: deterministic Kripke frames based on a Stone-type duality, weighted automata based on the self-duality of semimodules, and topological automata based on Gelfand duality. As a new example, we develop alternating automata based on the discrete duality between sets and complete atomic Boolean algebras. (shrink)

We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests. The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT. We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof.

It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the Π 1 1 relations. This extends a result of Harel and Kozen 118) relating IND and Π 1 1 over countable structures with some coding power, and provides a computational analog of a result of Barwise et al. 108) relating the Π 1 1 relations on a countable structure to a certain family of inductively definable relations on the hereditarily finite sets over that structure.