Order:
  1.  40
    A finite model theorem for the propositional μ-calculus.Dexter Kozen - 1988 - Studia Logica 47 (3):233 - 241.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  2.  25
    Minimisation in Logical Form.Nick Bezhanishvili, Marcello M. Bonsangue, Helle Hvid Hansen, Dexter Kozen, Clemens Kupke, Prakash Panangaden & Alexandra Silva - 2023 - In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 89-127.
    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 (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  3.  28
    KAT-ML: an interactive theorem prover for Kleene algebra with tests.Kamal Aboul-Hosn & Dexter Kozen - 2006 - Journal of Applied Non-Classical Logics 16 (1-2):9-33.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  4.  16
    Computational inductive definability.Dexter Kozen - 2004 - Annals of Pure and Applied Logic 126 (1-3):139-148.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark