{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T09:31:53Z","timestamp":1730280713438,"version":"3.28.0"},"reference-count":44,"publisher":"IEEE","license":[{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1109\/lics.2019.8785784","type":"proceedings-article","created":{"date-parts":[[2019,8,5]],"date-time":"2019-08-05T21:15:55Z","timestamp":1565039755000},"page":"1-14","source":"Crossref","is-referenced-by-count":8,"title":["HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories"],"prefix":"10.1109","author":[{"given":"C.-H. Luke","family":"Ong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"ref33","first-page":"92","article-title":"über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt","author":"presburger","year":"1929","journal-title":"Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_6"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"journal-title":"Mathematical theory of computation","year":"2003","author":"manna","key":"ref30"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_105"},{"key":"ref36","article-title":"Extending SMT solvers to higher-order logic","author":"barbosa","year":"2019","journal-title":"Technical Report"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.262.3"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_13"},{"key":"ref10","article-title":"A proof of the standardization theorem in lambda-calculus","author":"kashima","year":"2000","journal-title":"Tokyo Institute of Technology Research Reports on Mathematical and Computing Sciences C-145"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04222-5_5"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.2307\/2269949"},{"journal-title":"Constrained resolution A complete method for higher order logic","year":"1972","author":"huet","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054248"},{"key":"ref14","first-page":"28","article-title":"Super-position for lambda-free higher-order logic","author":"bentkamp","year":"2018","journal-title":"Automated Reasoning-9th International Joint Conference IJCAR 2018 Held as Part of the Federated Logic Conference FloC 2018"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785784"},{"key":"ref16","volume":"40","author":"barendregt","year":"2012","journal-title":"The lambda calculus its syntax and semantics ser Studies in Logic (London)"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499942"},{"key":"ref18","first-page":"1","article-title":"Domain theory","volume":"3","author":"abramsky","year":"1994","journal-title":"Handbook of Logic in Computer Science"},{"journal-title":"Model Theory","year":"2013","author":"chang","key":"ref19"},{"key":"ref28","article-title":"Undecidability of presburger arithmetic with a single monadic predicate letter","author":"downey","year":"1972","journal-title":"Technical Report TR-18-72"},{"journal-title":"A Mathematical Introduction to Logic","year":"2001","author":"enderton","key":"ref4"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-7066-3_4"},{"key":"ref29","article-title":"The universal fragment of Presburger arithmetic with unary uninterpreted predicates is undecidable","volume":"abs 1703 1212","author":"horbach","year":"2017","journal-title":"CoRR"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"journal-title":"Introduction to HOL A Theorem Proving Environment for Higher Order Logic","year":"1993","author":"gordon","key":"ref8"},{"key":"ref7","first-page":"229","article-title":"Higher order logic","author":"leivant","year":"1994","journal-title":"Handbook of Logic in Artificial Intelligence and Logic Programming"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-89901-9.50012-4"},{"key":"ref1","first-page":"11: 1","article-title":"Higher-order constrained Horn clauses for verification","volume":"2","author":"cathcart burn","year":"2018","journal-title":"PACMPL"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BF01190829"},{"key":"ref22","first-page":"275","author":"van benthem","year":"1983","journal-title":"Higher-Order Logic"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"ref42","article-title":"Defunctionalization of higher-order constrained Horn clauses","volume":"abs1810 3598","author":"pham","year":"2018","journal-title":"CoRR"},{"key":"ref24","first-page":"101","article-title":"Hammering towards QED","volume":"9","author":"blanchette","year":"2016","journal-title":"Journal of Formalized Reasoning"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"ref23","first-page":"137","article-title":"How to prove higher order theorems in first order logic","author":"kerber","year":"1991","journal-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429081"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_37"}],"event":{"name":"2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","start":{"date-parts":[[2019,6,24]]},"location":"Vancouver, BC, Canada","end":{"date-parts":[[2019,6,27]]}},"container-title":["2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8765678\/8785654\/08785784.pdf?arnumber=8785784","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T16:20:37Z","timestamp":1658247637000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8785784\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6]]},"references-count":44,"URL":"https:\/\/doi.org\/10.1109\/lics.2019.8785784","relation":{},"subject":[],"published":{"date-parts":[[2019,6]]}}}