{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:34Z","timestamp":1742617234220,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633853"},{"type":"electronic","value":"9783540698067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63385-5_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:26:19Z","timestamp":1330298779000},"page":"203-218","source":"Crossref","is-referenced-by-count":2,"title":["Comparing computational representations of Herbrand models"],"prefix":"10.1007","author":[{"given":"Robert","family":"Matzinger","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"C. Bourely, R. Caferra, and N. Peltier. A method for building models automatically. Experiments with an extension of otter. In Alan Bundy, editor, 12th International Conference on Automated Deduction, pages 72\u201386, Nancy\/France, June 1994. Springer Verlag, LNAI 814.","DOI":"10.1007\/3-540-58156-1_6"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"B. Bogaert and Sophie Tison. Equality and disequality constraints on direct subterms in tree automata. In A. Finkel, editor, Proc. 9th Annual Symposium on Theoretical Aspects of Computer Science, volume 577 of LNCS, pages 161\u2013172, Cachan, 1992. Springer.","DOI":"10.1007\/3-540-55210-3_181"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Anne-C\u00e9cile Caron, Jean-Luc Coquid\u00e9, and Max Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, Proc. 5th RTA, volume 690 of LNCS, pages 328\u2013342. Springer, June 1993.","DOI":"10.1007\/3-540-56868-9_25"},{"key":"17_CR4","first-page":"100","volume-title":"Proceedings 2nd International Workshop on Conditional and Typed Rewriting Systems","author":"H. Chen","year":"1990","unstructured":"H. Chen, J. Hsiang, and H.-C. Kong. On finite representations of infinite sequences of terms. In S. Kaplan and M. Okada, editors, Proceedings 2nd International Workshop on Conditional and Typed Rewriting Systems, volume 516 of LNCS, pages 100\u2013114, Montreal, Canada, June 1990. Springer."},{"key":"17_CR5","volume-title":"Symbolic Logic an Mechanical Theorem Proving","author":"C.-L. Chang","year":"1973","unstructured":"C.-L. Chang and R. C. T. Lee. Symbolic Logic an Mechanical Theorem Proving. Academic Press, New York, 1973."},{"issue":"34","key":"17_CR6","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon and P. Lescanne. Equational Problems and Disunification. Journal of Symbolic Computation, 7(34):371\u2013426, March\/April 1989.","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"17_CR7","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF01294596","volume":"28","author":"H. Comon","year":"1995","unstructured":"H. Comon. On unification of terms with integer exponents. Mathematical Systems Theory, 28(1):67\u201388, 1995.","journal-title":"Mathematical Systems Theory"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"R. Caferra and N. Peltier. Decision procedures using model building techniques. In Computer Science Logic (9th Int. Workshop CSL'95), pages 131\u2013144, Paderborn, Germany, 1995. Springer Verlag. LNCS 1092.","DOI":"10.1007\/3-540-61377-3_35"},{"issue":"6","key":"17_CR9","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"R. Caferra and N. Zabel. A method for simultanous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13(6):613\u2013641, June 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR10","series-title":"Computer Science Logic (CSL'92)","first-page":"134","volume-title":"Model building by resolution","author":"C. Ferm\u00fcller","year":"1993","unstructured":"C. Ferm\u00fcller and A. Leitsch. Model building by resolution. In Computer Science Logic (CSL'92), pages 134\u2013148, San Miniato, Italy, 1993. Springer Verlag. LNCS 702."},{"key":"17_CR11","unstructured":"C. Ferm\u00fcller and A. Leitsch. Decision procedures and model building in equational clause logic. Technical Report TR-CS-FL-96-1, TU Wien, Vienna\/Austria, 1996."},{"issue":"2","key":"17_CR12","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"C. Ferm\u00fcller and A. Leitsch. Hyperresolution and automated model building. J. of Logic and Computation, 6(2):173\u2013203, 1996.","journal-title":"J. of Logic and Computation"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"R. Galbavy and M. Hermann. Unification of infinite sets of terms schematized by primal grammars. Theoretical Computer Science, 176, April 1997.","DOI":"10.1016\/S0304-3975(96)00052-7"},{"key":"17_CR14","volume-title":"Tree Automata","author":"F. G\u00e9cseg","year":"1984","unstructured":"F. G\u00e9cseg and M. Steinby. Tree Automata. Akad\u00e9miai Kiad\u00f3, Budapest, 1984."},{"key":"17_CR15","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970."},{"key":"17_CR16","unstructured":"D. Loveland. Automated Theorem Proving \u2014 A Logical Basis. North Holland, 1978."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"R. Matzinger. Computational representations of Herbrand models using grammars. In D.v. Dalen, editor, Proceedings of the CSL'96, LNCS. Springer, 1997. To appear.","DOI":"10.1007\/3-540-63172-0_48"},{"key":"17_CR18","unstructured":"R. Matzinger. Context free term sets are regular-and some applications to logic. Technical Report TR-WB-Mat-97-2, TU Wien, Vienna\/Austria, 1997."},{"issue":"2","key":"17_CR19","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"23","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D.C. Oppen. Fast decision algorithms based on congruence closure. JACM, 23(2):356\u2013364, 1980.","journal-title":"JACM"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"G. Rozenberg and A. Salomaa, editors. Lindenmayer Systems. Springer, 1992.","DOI":"10.1007\/978-3-642-58117-5"},{"key":"17_CR21","volume-title":"Formal languages","author":"A. Salomaa","year":"1973","unstructured":"A. Salomaa. Formal languages. Academic Press, Orlando, 1973."},{"key":"17_CR22","unstructured":"G. Salzer. The unification of infinite sets of terms and its applications. In A. Voronkov, editor, Proceedings Logic Programming and Automated Reasoning, St. Petersburg (Russia), volume 624 of Lecture Notes in Computer Science (in Art. Intelligence). Springer, 1992."},{"key":"17_CR23","unstructured":"J. Slaney. FINDER (finite domain enumerator): Notes and guide. Technical Report TR-ARP-1\/92, Australien National University Automated Reasoning Project, Canberra, 1992."},{"key":"17_CR24","unstructured":"J. Slaney. SCOTT: A model-guided theorem prover. In Proceedings of the 13th international joint conference on artificial intelligence (IJCAI `93), volume 1, pages 109\u2013114. Morgan Kaufmann Publishers, 1993."},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"T. Tammet. Using resolution for deciding solvable classes and building finite models. In Baltic Computer Science, pages 33\u201364. Springer Verlag, 1991. LNCS 502.","DOI":"10.1007\/BFb0019355"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"C. Weidenbach. Unification in pseudo-linear sort theories is decidable. In M.A. McRobbie and J.K. Slaney, editors, Automated Deduction \u2014 Cade-13, LNAI 1104, pages 343\u2013357, New Brunswick, NJ, USA, July 1996. Springer-Verlag.","DOI":"10.1007\/3-540-61511-3_99"}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63385-5_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:43:04Z","timestamp":1742600584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63385-5_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633853","9783540698067"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-63385-5_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}