{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:59Z","timestamp":1725488939131},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_20","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"241-259","source":"Crossref","is-referenced-by-count":2,"title":["Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Gramlich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Pichler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"P. Baumgartner, C. Ferm\u00fcller, N. Peltier, and H. Zhang. Workshop: Model Computation-Principles, Algorithms, Applications. In D. McAllester, ed., Proc. 17th Int. Conf. on Automated Deduction (CADE\u201900), LNAI 1831, p. 513, Pittsburgh, PA, USA, June 2000. Springer-Verlag.","DOI":"10.1007\/10721959_45"},{"key":"20_CR3","unstructured":"R. Caferra and N. Peltier. Extending semantic resolution via automated model building: Applications. In Proc. 14th Int. Conf. on Artificial Intelligence (IJ-CAI\u201995), pp. 328\u2013334, Montr\u00e9al, Qu\u00e9bec, Canada, Aug. 1995. Morgan Kaufmann."},{"key":"20_CR4","doi-asserted-by":"publisher","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:613\u2013642, 1992.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1023\/A:1005875128672","volume":"18","author":"H. Chu","year":"1997","unstructured":"H. Chu and D. Plaisted. CLIN-S-a semantically guided first-order theorem prover. Journal of Automated Reasoning, 18(2):183\u2013188, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR6","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Preliminary version from October, 14 1999, available at: http:\/\/www.grappa.univ-lille3.fr\/tata ."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and D. Plaisted. Rewriting. In J. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume 1, chapter 9, pp. 535\u2013610. Elsevier and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"issue":"2","key":"20_CR8","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. G. Ferm\u00fcller","year":"1996","unstructured":"C. G. Ferm\u00fcller and A. Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2):173\u2013230, 1996.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"20_CR9","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1093\/jigpal\/6.1.17","volume":"6","author":"C. G. Ferm\u00fcller","year":"1998","unstructured":"C. G. Ferm\u00fcller and A. Leitsch. Decision procedures and model building in equational clause logic. Logic Journal of the IGPL, 6(1):17\u201341, 1998.","journal-title":"Logic Journal of the IGPL"},{"key":"20_CR10","unstructured":"Z. F\u00fcl\u00f6p and S. V\u00e1gv\u00f6lgyi. Ground term rewriting rules for the word problem of ground term equations. Bulletin of the European Association for Theoretical Computer Science, 45:186\u2013201, Oct. 1991."},{"key":"20_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1007\/3-540-48224-5_58","volume-title":"Proc. 28th International Colloquium on Automata, Languages and Programming (ICALP\u201901)","author":"G. Gottlob","year":"2001","unstructured":"G. Gottlob and R. Pichler. Hypergraphs in model checking: Acyclicity and hypertree-width versus clique-width. In F. Orejas, P. Spirakis, and J. Leeuwen, eds., Proc. 28th International Colloquium on Automata, Languages and Programming (ICALP\u201901), LNCS 2076, pp. 708\u2013719, Crete, Greece, July 201. Springer-Verlag."},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"B. Gramlich and R. Pichler. Algorithmic aspects of Herbrand models represented by ground atoms with ground equations. Technical report, Institut f\u00fcr Computersprachen, TU Wien, May 2002. Full version of this paper.","DOI":"10.1007\/3-540-45620-1_20"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"K. Hodgson and J. Slaney. System description: Scott-5. In R. Gor\u00e9, A. Leitsch, and T. Nipkow, eds., Proc. 1st Int. Joint Conf. on Automated Reasoning (IJCAR\u201901), LNAI 2083, pp. 443\u2013447, Siena, Italy, June 2001. Springer-Verlag.","DOI":"10.1007\/3-540-45744-5_36"},{"key":"20_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/3-540-63385-5_44","volume-title":"Proc. 5th Kurt G\u00f6del Colloquium-Computational Logic and Proof Theory (KGC\u201997)","author":"R. Matzinger","year":"1997","unstructured":"R. Matzinger. Comparing computational representations of Herbrand models. In G. Gottlob, A. Leitsch, and D. Mundici, eds., Proc. 5th Kurt G\u00f6del Colloquium-Computational Logic and Proof Theory (KGC\u201997), LNCS 1289, pp. 203\u2013218, Vienna, Austria, Aug. 1997. Springer-Verlag."},{"key":"20_CR15","unstructured":"R. Matzinger. Computational Representations of Models in First-Order Logic. PhD thesis, Vienna University of Technology, 2000."},{"issue":"1","key":"20_CR16","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/FI-1997-30105","volume":"30","author":"N. Peltier","year":"1997","unstructured":"N. Peltier. Tree automata and automated model building. Fundamenta Informaticae, 30(1):59\u201381, 1997.","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"20_CR17","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1006\/inco.1996.0028","volume":"125","author":"D. Plaisted","year":"1996","unstructured":"D. Plaisted and A. Sattler-Klein. Proof lengths for equational completion. Information and Computation, 125(2):154\u2013170, 1996.","journal-title":"Information and Computation"},{"issue":"3","key":"20_CR18","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1137\/0219027","volume":"19","author":"H. Seidl","year":"1990","unstructured":"H. Seidl. Deciding equivalence of finite tree automata. SIAM Journal on Computing,, 19(3):424\u2013437, June 1990.","journal-title":"SIAM Journal on Computing"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"J. Slaney. FINDER: Finite domain enumerator-system description. In A. Bundy, ed., Proc. 12th Int. Conf. on Automated Deduction (CADE\u201994), LNAI 814, pp. 798\u2013801, Nancy, France, June 26-July 1 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58156-1_63"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1006\/jsco.1993.1029","volume":"15","author":"W. Snyder","year":"1993","unstructured":"W. Snyder. A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. Journal of Symbolic Computation, 15:415\u2013450, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR21","series-title":"PhD thesis","volume-title":"Resolution Methods for Decision Problems and Finite Model Building","author":"T. Tammet","year":"1992","unstructured":"T. Tammet. Resolution Methods for Decision Problems and Finite Model Building. PhD thesis, Chalmers University of Technology, G\u00f6teborg, Sweden, 1992."},{"issue":"2","key":"20_CR22","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"S. Winker. Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions. Journal of the ACM, 29(2):273\u2013284, 1982.","journal-title":"Journal of the ACM"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"J. Zhang and H. Zhang. System description: Generating models by SEM. In M. McRobbie and J. Slaney, eds., Proc. 13th Int. Conf. on Automated Deduction (CADE\u201996), LNAI 1104, pp. 308\u2013312, New Brunswick, NJ, USA, July 30-August 3 1996. Springer-Verlag.","DOI":"10.1007\/3-540-61511-3_96"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T20:26:43Z","timestamp":1587846403000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}