{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T08:39:04Z","timestamp":1726043944113},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030301781"},{"type":"electronic","value":"9783030301798"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30179-8_6","type":"book-chapter","created":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:03:18Z","timestamp":1567969398000},"page":"76-86","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Human-Oriented Term Rewriting System"],"prefix":"10.1007","author":[{"given":"Edward William","family":"Ayers","sequence":"first","affiliation":[]},{"given":"William T.","family":"Gowers","sequence":"additional","affiliation":[]},{"given":"Mateja","family":"Jamnik","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,24]]},"reference":[{"key":"6_CR1","volume-title":"Term Rewriting and All that","author":"F Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All that. Cambridge University Press, Cambridge (1999)"},{"issue":"1\u20132","key":"6_CR2","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/S0004-3702(96)00047-1","volume":"90","author":"AL Blum","year":"1997","unstructured":"Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell. 90(1\u20132), 281\u2013300 (1997)","journal-title":"Artif. Intell."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107\u2013121. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111\u2013120. Springer, Heidelberg (1988). \n                    https:\/\/doi.org\/10.1007\/BFb0012826"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45632-5_7","volume-title":"Computational Logic: Logic Programming and Beyond","author":"A Bundy","year":"2002","unstructured":"Bundy, A.: A critique of proof planning. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2408, pp. 160\u2013177. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45632-5_7"},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10472-011-9248-8","volume":"61","author":"A Bundy","year":"2011","unstructured":"Bundy, A.: Automated theorem provers: a practical tool for the working mathematician? Ann. Math. Artif. Intell. 61(1), 3 (2011). \n                    https:\/\/doi.org\/10.1007\/s10472-011-9248-8","journal-title":"Ann. Math. Artif. Intell."},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98\u2013113. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/11541868_7"},{"key":"6_CR8","unstructured":"Hoek, K., Morrison, S.: Lean-rewrite-search repository (2019). \n                    https:\/\/github.com\/semorrison\/lean-rewrite-search"},{"issue":"1","key":"6_CR9","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0004-3702(94)00076-D","volume":"76","author":"S Kambhampati","year":"1995","unstructured":"Kambhampati, S., Knoblock, C.A., Yang, Q.: Planning as refinement search: a unified framework for evaluating design tradeoffs in partial-order planning. Artif. Intell. 76(1), 167\u2013238 (1995)","journal-title":"Artif. Intell."},{"key":"6_CR10","unstructured":"Langley, P., Choi, D., Trivedi, N.: Icarus user\u2019s manual. Institute for the Study of Learning and Expertise 2164 (2011)"},{"issue":"1","key":"6_CR11","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0004-3702(99)00076-4","volume":"115","author":"E Melis","year":"1999","unstructured":"Melis, E., Siekmann, J.: Knowledge-based proof planning. Artif. Intell. 115(1), 65\u2013105 (1999)","journal-title":"Artif. Intell."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L Moura de","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"6_CR13","unstructured":"Tate, A.: Generating project networks. In: Proceedings of the 5th International Joint Conference on Artificial Intelligence, vol. 2, pp. 888\u2013893. Morgan Kaufmann Publishers Inc. (1977)"}],"container-title":["Lecture Notes in Computer Science","KI 2019: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30179-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:38:08Z","timestamp":1567971488000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30179-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030301781","9783030301798"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30179-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"24 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"KI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Joint German\/Austrian Conference on Artificial Intelligence (K\u00fcnstliche Intelligenz)","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kassel","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"42","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ki2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.ki2019.de\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"82","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}