{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:30Z","timestamp":1725663750554},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540525318"},{"type":"electronic","value":"9783540470144"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52531-9_154","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:36:07Z","timestamp":1330205767000},"page":"278-279","source":"Crossref","is-referenced-by-count":0,"title":["Design and development of ENprover, an automated theorem proving system based on EN-strategy"],"prefix":"10.1007","author":[{"given":"Fabio","family":"Baj","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Bruschi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonella","family":"Zanzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,5]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"S.Anantharaman, J.Hsiang, J.Mazali, \"SbReve2: A Term Rewriting Laboratory with (AC-Unfailing Completion\", in RTA89, LNCS 355, 1989","DOI":"10.1007\/3-540-51081-8_131"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"J.Avenhaus, J.Denzinger, J.Muller, \"THEOPOGLES \u2014 An efficient Theorem Prover based on Rewrite-Techniques\", in RTA89, LNCS 355, 1989","DOI":"10.1007\/3-540-51081-8_132"},{"key":"37_CR3","unstructured":"F.Baj, \"Development of an ATP for FOPC+=\" (in Italian), Thesis, Comp. Sc. Dep. Milan, 1989"},{"key":"37_CR4","unstructured":"F.Baj, G.Ferrari, D.Galli, \"Theorem proving in supercomputing\", Supercomputing Tools for Science and Engineering \u2014 Workshop Proc., 1989"},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"M.P.Bonacina, G.Sanna, \"KBlab: An Equational Theorem Prover for the Macintosh\", in RTA89, LNCS 355, 1989","DOI":"10.1007\/3-540-51081-8_135"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"R.Boyer, E.Lusk, W.McCune, R.Overbeek, M.Stickel, L.Wos, \"Set theory in first order logic: clauses for Goedel axioms\", JAR 1, 1986","DOI":"10.1007\/BF02328452"},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"J.Christian, \"Fast Knuth-Bendix Completion: Summary\", in RTA89, LNCS355, 1989","DOI":"10.1007\/3-540-51081-8_136"},{"key":"37_CR8","unstructured":"N.Dershowitz, J.Hsiang, \"Rewrite methods for clausal and non-clausal theorem proving\", Proc. ICALP 83, LNCS 154, 1983"},{"key":"37_CR9","unstructured":"G.Ferrari, \"ENprover in C Language on Transputers\" (in Italian), Thesis, Comp. Sc. Dep. of Milan, 1989"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"J.Hsiang, \"Refutational Theorem Proving Using Term Rewriting Systems\", AI J. 1985, Manuscript, Univ of Illinois at Urbana, Dep. Comp. Scie., 1981","DOI":"10.1016\/0004-3702(85)90074-8"},{"key":"37_CR11","unstructured":"J.Hsiang, \"Topics in Automated Theorem Proving and Program Generation\", AI J., 1985, PhD Thesis, Univ of Illinois at Urbana, Dep. Comp. Scie., 1982"},{"key":"37_CR12","doi-asserted-by":"crossref","unstructured":"J.Hsiang, \"Refutational theorem proving using term rewriting systems\", Art. Int. 25, 1985","DOI":"10.1016\/0004-3702(85)90074-8"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"J.Hsiang, \"Rewrite Method for Theorem Proving in First Order Theory with Equality\", J. Symb. Comp., 1987","DOI":"10.1016\/S0747-7171(87)80024-X"},{"key":"37_CR14","unstructured":"J.Hsiang, N.A.Josephson, \"TeRSe: A Rewriting Theorem Prover\", in Proc. Rewrite Rule Laboratory Workshop, Schenectady, NY, 1983"},{"key":"37_CR15","unstructured":"D.Kalish, R.Montague, \"Logic, thechniques of formal reasoning\", H.Brace & World Inc, 1964"},{"key":"37_CR16","doi-asserted-by":"crossref","unstructured":"D.Kapur, H.Zhang, \"An Overview of Rewrite Rule Laboratory (RRL)\", in RTA89, LNCS 355, 1989","DOI":"10.1007\/3-540-51081-8_138"},{"key":"37_CR17","unstructured":"G.Leidi, \"An ATP for FOPC+=\" (in Italian), Thesis, Comp. Sc. Dep. Milan, 1988"},{"key":"37_CR18","unstructured":"W.W.McCune, OTTER 1.0 Users' Guide, Argonne National Lab. Report, ANL-88-44, 1989"},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"F.J.Pelletier, \"Seventy-five problems for testing automatic theorem provers\", JAR 2, 1986","DOI":"10.1007\/BF02432151"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"B.Smith, R.Wilkerson, \"Non-Obviousness \u2014 Again\", AAR Newsletter 11, 1989","DOI":"10.1016\/0196-4399(89)90029-9"}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52531-9_154.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:24:32Z","timestamp":1605648272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52531-9_154"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540525318","9783540470144"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-52531-9_154","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}