{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T20:14:09Z","timestamp":1672344849447},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1989,9,1]],"date-time":"1989-09-01T00:00:00Z","timestamp":620611200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1989,9]]},"DOI":"10.1007\/bf00248322","type":"journal-article","created":{"date-parts":[[2004,10,5]],"date-time":"2004-10-05T13:40:08Z","timestamp":1096983608000},"page":"309-337","source":"Crossref","is-referenced-by-count":10,"title":["Horn equational theories and paramodulation"],"prefix":"10.1007","volume":"5","author":[{"given":"Ulrich","family":"Furbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steffen","family":"H\ufffdlldobler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Schreiber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"653","volume":"36","author":"R. Anderson","year":"1970","unstructured":"Anderson, R., ?Completeness Results for E-resolution?, Proc. AFIPS Spring Joint Computer Conference, 36, 653?656 (1970).","journal-title":"Proc. AFIPS Spring Joint Computer Conference"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Apt, K. A., and van Emden, M. H., ?Contributions to the Theory of Logic Programming?, J. ACM, 841?862 (1982).","DOI":"10.1145\/322326.322339"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D., ?Proving Theorems With The Modification Method?, SIAM J. Comput. 4, 412?430 (1975).","journal-title":"SIAM J. Comput"},{"key":"CR4","unstructured":"Chang, C. L., and Lee, R. C. T., Symbolic Logic and Mechanical Theorem Proving, Academic Press: 1973."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0168-0072(86)90069-2","volume":"31","author":"P. T. Cox","year":"1986","unstructured":"Cox, P. T., and Pietrzykowski, T., ?Incorporating Equality in Logic Programming via Surface Deduction?, Annals of Pure and Applied Logic 31, 177?189 (1986).","journal-title":"Annals of Pure and Applied Logic"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"van Emden, M. H., and Kowaslki, R. A., ?The Semantics of Predicate Logic as a Programming Language?, J. ACM 733?742 (1976).","DOI":"10.1145\/321978.321991"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Fribourg, L., ?Oriented Equational Clauses as a Programming Language?, J. Logic Programming, 165?177 (1984).","DOI":"10.1007\/3-540-13345-3_15"},{"key":"CR8","unstructured":"Furbach, U., ?Oldy but Goody: Paramodulation Revisited? Proc. GWAI '87 (Morik ed.), Informatik Fachberichte 152, 195?200 (1987)."},{"key":"CR9","unstructured":"Gallier, J. H., and Raatz, S., ?SLD-resolution Methods for Horn Clauses with Equality based on E-unification?, Proc. Symposium on Logic Programming, 168?179 (1986)."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Gallier, J. H., and Raatz, S., ?Extending SLD-resolution to Equational Horn Clauses Using E-unification?, To appear in J. Logic programming: 1988.","DOI":"10.1016\/0743-1066(89)90028-9"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Gallier, J. H., and Snyder, W., ?A Complete E-Unification Procedure?, Proc. RTA, LNCS 256 (1987).","DOI":"10.1007\/3-540-17220-3_19"},{"key":"CR12","volume-title":"Complete Sets of Transformations for General E-Unification","author":"J. H. Gallier","year":"1987","unstructured":"Gallier, J. H., and Snyder, W., ?Complete Sets of Transformations for General E-Unification?. Univ. of Pennsylvania, Philadelphia: 1987."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Giovannetti, E., and Moiso, C., ?A Completeness Result for E-Unification Algorithms Based on Conditional Narrowing?, Proc. Workshop on Foundations of Logic and Functional programming (to appear in LNCS) (1987).","DOI":"10.1007\/3-540-19129-1_7"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Goguen, J. A., and Meseguer, J., ?Equality, Types, and Generics for Logic programming?. J. Logic Programming 179?210 (1984).","DOI":"10.1016\/0743-1066(84)90004-9"},{"key":"CR15","unstructured":"Goguen, J. A., and Meseguer, J., ?EQLOG: Equality, Types, and Generic Modules for Logic Programming?, in: Logic Programming (DeGroot, Lindstrom, eds.), Prentice Hall, 295?363 (1986)."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1145\/321850.321857","volume":"21","author":"L. Henschen","year":"1974","unstructured":"Henschen, L., and Wos, L., ?Unit refutations and Horn sets?, J. ACM, 21, 590?604 (1974).","journal-title":"J. ACM"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Herbrand, J., ?Sur la Th\u00e9orie de la D\u00e9monstration?, Logical Writings (Goldfarb, ed.), Cambridge (1971).","DOI":"10.1007\/978-94-010-3072-4"},{"key":"CR18","unstructured":"Hill, R., ?LUSH-Resolution and its Completeness?, DCI Memo 78, University of Edinburgh (1974)."},{"key":"CR19","first-page":"54","volume":"267","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., and Rusinowitch, M., ?On Word Problems in Equational Theories?, Proc. ICALP, LNCS 267, 54?71 (1987).","journal-title":"Proc. ICALP, LNCS"},{"key":"CR20","unstructured":"H\u00f6lldobler, S., ?From Paramodulation to Narrowing?. Proc. 5th International Conference Symposium on Logic Programming, 327?342 (1988)."},{"key":"CR21","unstructured":"H\u00f6lldobler, S., ?Horn Equality Theories and Complete Sets of Transformations?. Proc. International Conference on the Fifth Generation Computer Systems, 405?412 (1988)."},{"key":"CR22","unstructured":"H\u00f6lldobler, S., ?SLDE-resolution?, UniBwM (1988) (submitted)."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Hullot, J. M., ?Canonical Forms and Unification?, Proc. 5th Conf. Automated Deduction, 318?334 (1980).","DOI":"10.21236\/ADA087640"},{"key":"CR24","first-page":"543","volume":"204","author":"H. Hussmann","year":"1985","unstructured":"Hussmann, H., ?Unification in Conditional Equational Theories?, LNCS 204, 543?553 (1985).","journal-title":"LNCS"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J-L., and Maher, M., ?A Theory of Complete Logic Programs with Equality?. Proc. FGCS '84, 175?184 (1984).","DOI":"10.1016\/0743-1066(84)90010-4"},{"key":"CR26","unstructured":"Jaffar, J., Lassez, J-L., and Maher, M., ?A Logic Programming Language Scheme?. In: Logic Programming (DeGroot, Lindstrom, eds.), Prentice Hall, 441?467 (1986)."},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"Martelli, A., and Montanari, U., ?An Efficient Unification Algorithm?, ACM TOPLAS, 258?282 (1982).","DOI":"10.1145\/357162.357169"},{"key":"CR28","unstructured":"Martelli, A., Moiso, C., and Rossi, C. F., ?An Algorithm for Unification in Equational Theories?, Proc. SLP '86, 180?186 (1986)."},{"key":"CR29","unstructured":"Morris, J., ?E-resolution: An Extension of Resolution to include the Equality Relation?. Proc. IJCAI, 287?294 (1987)."},{"key":"CR30","first-page":"136","volume":"116","author":"S. Kaplan","year":"1986","unstructured":"Kaplan, S., ?Fair Conditional Term Rewriting Systems: Unification, Termination and Confluence?, IFB 116, 136?155 (1986).","journal-title":"IFB"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"Lloyd, J. W., Foundations of Logic Programming, Springer (1984).","DOI":"10.1007\/978-3-642-96826-6"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. E. Peterson","year":"1983","unstructured":"Peterson, G. E., ?A Technique for Establishing Completeness Results in Theorem Proving With Equality?, SIAM J. Comput. 12, 82?100 (1983).","journal-title":"SIAM J. Comput."},{"key":"CR33","unstructured":"Plotkin, G. D., ?Building-In Equational Theories?, in: Machine Intelligence 7 (Meltzer, Mitchie, eds.), 73?90 (1972)."},{"key":"CR34","unstructured":"Robinson, G. A. and Wos, L., ?Paramodulation and Theorem Proving in First Order Theories with Equality?, in: Machine Intelligence 4 (Meltzer, Michie, eds.), 135?150 (1969)."},{"key":"CR35","doi-asserted-by":"crossref","unstructured":"Robinson, J. A., ?A Machine Oriented Logic based on the Resolution Principle?, J. ACM, 23?41 (1965).","DOI":"10.1007\/978-3-642-81952-0_26"},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"Robinson, J. A., ?A Review on Automatic Theorem Proving?, Annual Symposia in Applied Mathematics, 1?18 (1967).","DOI":"10.1090\/psapm\/019\/0241195"},{"key":"CR37","doi-asserted-by":"crossref","unstructured":"Slagle, J. R., ?Automatic Theorem Proving with Built-in Theories including Equality, Partial Orderings and Sets?, J. ACM 120?135 (1972).","DOI":"10.1145\/321679.321689"},{"key":"CR38","doi-asserted-by":"crossref","unstructured":"Wos, L., ?The Problem of Finding a Strategy to Control Binary Paramodulation?, J. Automated Reasoning, 101?107 (1988).","DOI":"10.1007\/BF00244514"},{"key":"CR39","doi-asserted-by":"crossref","unstructured":"Wos, L., and Robinson, G. A., ?Maximal Models and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving?, in: Word Problems (Boone, Cannonito, Lyndon, eds.), 609?639 (1973).","DOI":"10.1016\/S0049-237X(08)71923-2"},{"key":"CR40","doi-asserted-by":"crossref","unstructured":"Wos, L., Robinson, G. A., Carson, D., and Shalla, L., ?The Concept of Demodulation in Theorem Proving?, J. ACM 698?709 (1967).","DOI":"10.1007\/978-3-642-81955-1_5"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00248322.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00248322\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00248322","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T08:19:25Z","timestamp":1585901965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00248322"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,9]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1989,9]]}},"alternative-id":["BF00248322"],"URL":"https:\/\/doi.org\/10.1007\/bf00248322","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,9]]}}}