Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Halting and Equivalence of Schemes over Recursive Theories
Authors: Kozen, Dexter
Keywords: computer science
technical report
Issue Date: 28-Oct-2002
Publisher: Cornell University
Abstract: Let S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, a program scheme p over S, and input values specified by ground terms t1,...,tn, does p halt on input t1,...,tn in all models of T? (ii) Given a recursive ground theory T over S and two program schemes p and q over S, are p and q equivalent in all models of T? When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is r.e.-complete and problem (ii) is Pi-0-2-complete. Both these problems remain hard for their respective complexity classes even if T is empty and S is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File SizeFormat
2002-1881.ps113.81 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us