{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:14:54Z","timestamp":1754482494758},"reference-count":42,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1994,10,1]],"date-time":"1994-10-01T00:00:00Z","timestamp":780969600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":6864,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1994,10]]},"DOI":"10.1016\/0304-3975(94)90192-9","type":"journal-article","created":{"date-parts":[[2002,10,10]],"date-time":"2002-10-10T17:49:49Z","timestamp":1034272189000},"page":"307-339","source":"Crossref","is-referenced-by-count":23,"title":["An overview of the Tecton proof system"],"prefix":"10.1016","volume":"133","author":[{"given":"D.","family":"Kapur","sequence":"first","affiliation":[]},{"given":"X.","family":"Nie","sequence":"additional","affiliation":[]},{"given":"D.R.","family":"Musser","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(94)90192-9_BIB1","doi-asserted-by":"crossref","first-page":"820","DOI":"10.1145\/48511.48513","article-title":"KMS: a distributed hypermedia system for managing knowledge in organizations","volume":"31","author":"Akscyn","year":"1988","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(94)90192-9_BIB2","series-title":"The Handbook of Artificial Intelligence","author":"Barr","year":"1981"},{"key":"10.1016\/0304-3975(94)90192-9_BIB3","series-title":"Specification and Design Assistant, User's Manual","author":"Toolkit","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB4","series-title":"A Computational Logic Handbook","author":"Boyer","year":"1988"},{"key":"10.1016\/0304-3975(94)90192-9_BIB5","first-page":"83","article-title":"Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic","volume":"11","author":"Boyer","year":"1988","journal-title":"Mach. Intell."},{"issue":"9","key":"10.1016\/0304-3975(94)90192-9_BIB6","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1109\/MC.1987.1663693","article-title":"Hypertext: an introduction and survey","volume":"2","author":"Conklin","year":"1987","journal-title":"IEEE Comput."},{"key":"10.1016\/0304-3975(94)90192-9_BIB7","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/0304-3975(94)90192-9_BIB8","first-page":"766","article-title":"Eves system description","volume":"Vol. 607","author":"Craigen","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB9","series-title":"Proc. VDM'91, Formal Software Development Methods, Vol. 1","first-page":"689","article-title":"The CRI Raise tools group, the Raise toolset","volume":"Vol. 551","year":"1991"},{"key":"10.1016\/0304-3975(94)90192-9_BIB10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(94)90192-9_BIB11","series-title":"Proc. 5th Conf. on Automated Deduction","article-title":"The AFFIRM theorem prover: proof forests and management of large proofs","volume":"Vol. 87","author":"Erickson","year":"1980"},{"key":"10.1016\/0304-3975(94)90192-9_BIB12","series-title":"Proc. VDM'91, Formal Software Development Methods, Vol. 2","first-page":"239","article-title":"The RAISE specification language: a tutorial","volume":"Vol. 552","author":"George","year":"1991"},{"key":"10.1016\/0304-3975(94)90192-9_BIB13","series-title":"Applications of Algebraic Specification using OBJ","article-title":"Introducing OBJ","author":"Goguen","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB14","series-title":"VLSI Specification, Verification and Synthesis","article-title":"A proof generating system for higher order logic","author":"Gordon","year":"1987"},{"key":"10.1016\/0304-3975(94)90192-9_BIB15","article-title":"Edinburgh LCF","volume":"Vol. 78","author":"Gordon","year":"1979"},{"issue":"2","key":"10.1016\/0304-3975(94)90192-9_BIB16","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0167-6423(86)90021-3","article-title":"Report on the larch shared language","volume":"6","author":"Guttag","year":"1986","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(94)90192-9_BIB17","series-title":"Texts and Monographs in Computer Science","article-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag","year":"1993"},{"key":"10.1016\/0304-3975(94)90192-9_BIB18","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(94)90192-9_BIB19","article-title":"Tecton: a framework for specifying and verifying generic system components","author":"Kapur","year":"1992","journal-title":"Rensselaer Polytechnic Institute Computer Science Technical Report 92-20"},{"key":"10.1016\/0304-3975(94)90192-9_BIB20","unstructured":"D. Kapur and D.R. Musser, Examples of Tecton concept descriptions, in preparation."},{"key":"10.1016\/0304-3975(94)90192-9_BIB21","series-title":"The Tecton Proof System: Introduction and User's Guide","author":"Kapur","year":"1991"},{"key":"10.1016\/0304-3975(94)90192-9_BIB22","series-title":"Formal Methods in Databases and Software Engineering","first-page":"54","article-title":"The Tecton proof system","author":"Kapur","year":"1993"},{"key":"10.1016\/0304-3975(94)90192-9_BIB23","article-title":"Operators and algebraic structures","author":"Kapur","year":"1981","journal-title":"Proc. Conf. on Functional Programming Languages and Computer Architecture"},{"key":"10.1016\/0304-3975(94)90192-9_BIB24","article-title":"Tecton: a language for manipulating generic objects","volume":"Vol. 134","author":"Kapur","year":"1982"},{"key":"10.1016\/0304-3975(94)90192-9_BIB25","unstructured":"D. Kapur, D.R. Musser and C. Wang, Specification and verification of a generic partitioning algorithm, in preparation."},{"key":"10.1016\/0304-3975(94)90192-9_BIB26","series-title":"Reasoning about numbers in Tecton","author":"Kapur","year":"1994"},{"key":"10.1016\/0304-3975(94)90192-9_BIB27","article-title":"An overview of Rewrite Rule Laboratory (RRL)","author":"Kapur","year":"1994","journal-title":"Computers in Mathematics with Applications (a special issue)"},{"key":"10.1016\/0304-3975(94)90192-9_BIB28","unstructured":"R.A. Kemmerer, Verification Assessment Study Final Report, Vols. 1\u20135, National Computer Security Center, Fort George G. Meade, MD."},{"key":"10.1016\/0304-3975(94)90192-9_BIB29","series-title":"Lego Proof Development System: User's Manual","author":"Luo","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB30","series-title":"Machine support for formal methods: an overview of Mural","author":"Moore","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB31","series-title":"Elements of a pragmatic approach to program verification","author":"Musser","year":"1989"},{"key":"10.1016\/0304-3975(94)90192-9_BIB32","series-title":"The Ada Generic Library: Linear List Processing Packages","author":"Musser","year":"1989"},{"issue":"2","key":"10.1016\/0304-3975(94)90192-9_BIB33","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","article-title":"Simplification by cooperating decision procedures","volume":"1","author":"Nelson","year":"1979","journal-title":"ACM Trans. Programming Languages Systems"},{"key":"10.1016\/0304-3975(94)90192-9_BIB34","series-title":"Proc. Automated Deduction \u2014 CADE-11","first-page":"673","article-title":"Isabelle-91","volume":"Vol. 607","author":"Nipkow","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB35","series-title":"Proc. Automated Deduction \u2014 CADE-11 Saratoga","first-page":"748","article-title":"PVS: a prototype verification system","volume":"Vol. 1607","author":"Owre","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB36","doi-asserted-by":"crossref","DOI":"10.1016\/0167-6423(83)90008-4","article-title":"A higher-order implementation of rewriting","author":"Paulson","year":"1983","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(94)90192-9_BIB37","series-title":"Technical Report 80","article-title":"Interactive theorem proving with Cambridge LCF: a user's manual","author":"Paulson","year":"1985"},{"key":"10.1016\/0304-3975(94)90192-9_BIB38","series-title":"Introduction to Isabelle","author":"Paulson","year":"1993"},{"issue":"2","key":"10.1016\/0304-3975(94)90192-9_BIB39","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","article-title":"A practical decision procedure for arithmetic with function symbols","volume":"26","author":"Shostak","year":"1979","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(94)90192-9_BIB40","article-title":"Real theorem provers deserve real user-interfaces","author":"Th\u00e9ry","year":"1992","journal-title":"Univ. of Cambridge Report"},{"key":"10.1016\/0304-3975(94)90192-9_BIB41","series-title":"Proc. 3rd Internat. Workshop on Conditional Term Rewriting Systems","first-page":"363","article-title":"Implementing contextual rewriting","volume":"Vol. 656","author":"Zhang","year":"1992"},{"key":"10.1016\/0304-3975(94)90192-9_BIB42","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0012831","article-title":"A mechanizable induction principle for equational specifications","author":"Zhang","year":"1988","journal-title":"Proc. of 9th Internat. Conf. on Automated Deduction (CADE-9)"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397594901929?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397594901929?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T17:52:34Z","timestamp":1555177954000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397594901929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,10]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,10]]}},"alternative-id":["0304397594901929"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(94)90192-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1994,10]]}}}