Show simple item record

dc.contributor.authorKozen, Dexteren_US
dc.date.accessioned2007-04-09T19:57:53Z
dc.date.available2007-04-09T19:57:53Z
dc.date.issued2002-10-28en_US
dc.identifier.citationhttp://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1881en_US
dc.identifier.urihttps://hdl.handle.net/1813/5857
dc.description.abstractLet 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.en_US
dc.format.extent116540 bytes
dc.format.mimetypeapplication/postscript
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleHalting and Equivalence of Schemes over Recursive Theoriesen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics