{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:34:33Z","timestamp":1774060473799,"version":"3.50.1"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[1994,5,1]],"date-time":"1994-05-01T00:00:00Z","timestamp":767750400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[1994,5]]},"DOI":"10.1007\/bf01190829","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T06:25:56Z","timestamp":1108707956000},"page":"193-212","source":"Crossref","is-referenced-by-count":73,"title":["Refutational theorem proving for hierarchic first-order theories"],"prefix":"10.1007","volume":"5","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"Avenhaus, J., Becker, K.: Conditional rewriting modulo a built-in algebra. SEKI Report SR-92-11, Fachbereich Informatik, Universit\u00e4t Kaiserslautern (1992)"},{"key":"CR2","first-page":"427","volume-title":"Lecture Notes in Artificial Intelligence, Vol.449","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M. E. (ed.) 10th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, Vol.449, pp. 427?441. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR3","unstructured":"Bachmair, L., Ganzinger, H.: Perfect model semantics for logic programs with equality. In: Furukawa, K. (ed.) Logic Programming, Proceedings of the Eighth International Conference, pp. 645?659. The MIT Press 1991"},{"key":"CR4","volume-title":"Tech. Rep. MPI-I-91-208","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Tech. Rep. MPI-I-91-208, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (1991). Revised version to appear in J. Logic Comput."},{"key":"CR5","first-page":"193","volume-title":"Lecture Notes in Computer Science, Vol.118","author":"J. A. Bergstra","year":"1981","unstructured":"Bergstra, J. A., Broy, M., Tucker, J. V., Wirsing, M.: On the power of algebraic specifications. In: Gruska, J., Chytil, M. (eds.) Mathematical Foundations of Computer Science, 10th Symposium. Lecture Notes in Computer Science, Vol.118, pp. 193?204. Berlin, Heidelberg, New York: Springer 1981"},{"key":"CR6","first-page":"178","volume-title":"Lecture Notes in Artificial Intelligence, Vol.449","author":"H.-J. B\u00fcrckert","year":"1990","unstructured":"B\u00fcrckert, H.-J.: A resolution principle for clauses with constraints. In: Stickel, M. E. (ed.) 10th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, Vol.449, pp. 178?192. Berlin, Heidelberg, New York: Springer 1990"},{"key":"CR7","volume-title":"Lecture Notes in Artificial Intelligence, Vol.568","author":"H.-J. B\u00fcrckert","year":"1991","unstructured":"B\u00fcrckert, H.-J.: A Resolution Principle for a Logic with Restricted Quantifiers. Lecture Notes in Artificial Intelligence, Vol.568. Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR8","first-page":"244","volume-title":"Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, pp. 244?320. Amsterdam, New York, Oxford, Tokyo: Elsevier Science Publishers B. V. 1990"},{"key":"CR9","first-page":"35","volume":"7","author":"D. Gabbay","year":"1992","unstructured":"Gabbay, D., Ohlbach, H. J.: Quantifier elimination in second order predicate logic. South African Computer Journal7, 35?43 (1992). Also appeared in 3rd International Conference on Principles of Knowledge Representation and Reasoning, pp. 425?435. 1992","journal-title":"South African Computer Journal"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Fourteenth Annual ACM Symposium on Principles of Programming Languages, pp. 111?119 (1987)","DOI":"10.1145\/41625.41635"},{"key":"CR11","first-page":"174","volume-title":"Lecture Notes in Computer Science, Vol.448","author":"H. Kirchner","year":"1991","unstructured":"Kirchner, H.: Proofs in parameterized specifications. In: Book, R. V. (ed.) Rewriting Techniques and Applications, 4th International Conference. Lecture Notes in Computer Science, Vol.448, pp. 174?187. Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR12","volume-title":"Elements of Mathematical Logic","author":"G. Kreisel","year":"1967","unstructured":"Kreisel, G., Krivine, J.-L.: Elements of Mathematical Logic. Amsterdam: North-Holland 1967"},{"key":"CR13","unstructured":"Nieuwenhuis, R.: First-order completion techniques. Technical report, Universidad Polit\u00e9cnica de Catalu\u00f1a, Dept. Lenguajes y Sistemas Inform\u00e1ticos (1991)"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. E. Stickel","year":"1985","unstructured":"Stickel, M. E.: Automated deduction by theory resolution. J. Autom. Reasoning1, 333?355 (1985)","journal-title":"J. Autom. Reasoning"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-009-6259-0_4","volume-title":"Handbook of Philosophical Logic, Vol. II: Extensions of Classical Logic","author":"J. Benthem Van","year":"1984","unstructured":"Van Benthem, J.: Correspondence theory. In: Gabbay, D. M., Guenthner, F. (eds.) Handbook of Philosophical Logic, Vol. II: Extensions of Classical Logic, pp. 167?247. Dordrecht, Boston, Lancaster: D. Reidel 1984"},{"key":"CR16","first-page":"675","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"M. Wirsing","year":"1990","unstructured":"Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pp. 675?788. Amsterdam, New York, Oxford, Tokyo: Elsevier Science Publishers B. V. 1990"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01190829.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01190829\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01190829","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T09:08:23Z","timestamp":1556615303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01190829"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,5]]},"references-count":16,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1994,5]]}},"alternative-id":["BF01190829"],"URL":"https:\/\/doi.org\/10.1007\/bf01190829","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,5]]}}}