Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Some Results in Dynamic Model Theory

Some Results in Dynamic Model Theory

File(s)
2002-1882.ps (424.82 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5858
Collections
Computer Science Technical Reports
Author
Kozen, Dexter
Abstract

First-order structures over a fixed signature S give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are valuations of program variables and whose atomic actions are state changes effected by variable assignments x := e, where e is an S-term. The Kleene algebras with tests that arise in this way play a role in dynamic model theory akin to the role played by Lindenbaum algebras in classical first-order model theory. Given a first-order theory T over S, we exhibit a Kripke frame U whose trace algebra Tr U is universal for the equational theory of Tarskian trace algebras over S satisfying T, although U itself is not Tarskian in general. The corresponding relation algebra Rel U is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence.

Date Issued
2002-10-31
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1882
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance