{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:51Z","timestamp":1767928491614,"version":"3.49.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1527395"],"award-info":[{"award-number":["1527395"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>\n            We give foundational results that explain the efficacy of heuristics used for dealing with quantified formulas and recursive definitions. We develop a framework for first order logic (FOL) over an uninterpreted combination of background theories. Our central technical result is that systematic term instantiation is\n            <jats:italic>complete<\/jats:italic>\n            for a fragment of FOL that we call\n            <jats:italic>safe<\/jats:italic>\n            . Coupled with the fact that unfolding recursive definitions is essentially term instantiation and with the observation that heap verification engines generate verification conditions in the safe fragment explains the efficacy of verification engines like natural proofs that resort to such heuristics. Furthermore, we study recursive definitions with least fixpoint semantics and show that though they are not amenable to complete procedures, we can systematically introduce induction principles that in practice bridge the divide between FOL and FOL with recursive definitions.\n          <\/jats:p>","DOI":"10.1145\/3158098","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Foundations for natural proofs and quantifier instantiation"],"prefix":"10.1145","volume":"2","author":[{"given":"Christof","family":"L\u00f6ding","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucas","family":"Pe\u00f1a","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Aharon Abadi Alexander Rabinovich and Mooly Sagiv. 2007. Decidable Fragments of Many-sorted Logic. In LPAR\u201907. 17\u201331. http:\/\/dl.acm.org\/citation.cfm?id=1779419.1779423  Aharon Abadi Alexander Rabinovich and Mooly Sagiv. 2007. Decidable Fragments of Many-sorted Logic. In LPAR\u201907. 17\u201331. http:\/\/dl.acm.org\/citation.cfm?id=1779419.1779423","DOI":"10.1007\/978-3-540-75560-9_4"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01048403"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_2_6_1","volume-title":"A computational logic","author":"Boyer Robert S.","unstructured":"Robert S. Boyer and J. Strother Moore . 1980. A computational logic . Academic Press . Robert S. Boyer and J. Strother Moore. 1980. A computational logic. Academic Press."},{"key":"e_1_2_2_8_1","volume-title":"Bradley and Zohar Manna","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna . 2007 . The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag New York , Inc., Secaucus, NJ, USA. Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag New York, Inc., Secaucus, NJ, USA."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_12"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737984"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_2_13_1","volume-title":"Z3: An Efficient SMT Solver","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . Springer Berlin Heidelberg , Berlin, Heidelberg , 337\u2013340. Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. Springer Berlin Heidelberg, Berlin, Heidelberg, 337\u2013340."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_2_16_1","volume-title":"Mathematical logic (2. ed.)","author":"Ebbinghaus Heinz-Dieter","unstructured":"Heinz-Dieter Ebbinghaus , J\u00f6rg Flum , and Wolfgang Thomas . 1994. Mathematical logic (2. ed.) . Springer . Heinz-Dieter Ebbinghaus, J\u00f6rg Flum, and Wolfgang Thomas. 1994. Mathematical logic (2. ed.). Springer."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210045"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_34"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.41.0028"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-21593-8"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"e_1_2_2_25_1","unstructured":"Bart Jacobs and Frank Piessens. 2008. The VeriFast Program Verifier. (2008).  Bart Jacobs and Frank Piessens. 2008. The VeriFast Program Verifier. (2008)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_2_2_27_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann Matt","unstructured":"Matt Kaufmann , J. Strother Moore , and Panagiotis Manolios . 2000. Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , Norwell, MA, USA . Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell, MA, USA."},{"key":"e_1_2_2_28_1","volume-title":"Giesl and R. H\u00e4hnle (Eds.)","volume":"6173","author":"Korovin K.","unstructured":"K. Korovin and C. Sticksel . 2010. iProver-Eq: An Instantiation-Based Theorem Prover with Equality. In IJCAR\u201910 (Lecture Notes in Computer Science), J . Giesl and R. H\u00e4hnle (Eds.) , Vol. 6173 . Springer, 196\u2013202. K. Korovin and C. Sticksel. 2010. iProver-Eq: An Instantiation-Based Theorem Prover with Equality. In IJCAR\u201910 (Lecture Notes in Computer Science), J. Giesl and R. H\u00e4hnle (Eds.), Vol. 6173. Springer, 196\u2013202."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958033"},{"key":"e_1_2_2_30_1","unstructured":"Q. L. (Quang Loc) Le M. Tatsuta J. ( Jun) Sun and W. N. (Wei-Ngan) Chin. 2017. A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. In CAV\u201917. http:\/\/hdl.handle.net\/10149\/621090  Q. L. (Quang Loc) Le M. Tatsuta J. ( Jun) Sun and W. N. (Wei-Ngan) Chin. 2017. A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. In CAV\u201917. http:\/\/hdl.handle.net\/10149\/621090"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Christof L\u00f6ding Parthasarathy Madhusudan and Lucas Pe\u00f1a. 2017. Foundations for Natural Proofs and Quantifier Instantiation: Artifact. https:\/\/github.com\/lucaspena\/foundations- np- qi- artifcat . (2017).  Christof L\u00f6ding Parthasarathy Madhusudan and Lucas Pe\u00f1a. 2017. Foundations for Natural Proofs and Quantifier Instantiation: Artifact. https:\/\/github.com\/lucaspena\/foundations- np- qi- artifcat . (2017).","DOI":"10.1145\/3158098"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926455"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_8"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_2_2_37_1","first-page":"79","article-title":"Properties of Programs and Partial Function Logic","volume":"5","author":"Manna Zohar","year":"1970","unstructured":"Zohar Manna and John McCarthy . 1970 . Properties of Programs and Partial Function Logic . Machine Intelligence 5 (1970), 79 \u2013 98 . Zohar Manna and John McCarthy. 1970. Properties of Programs and Partial Function Logic. Machine Intelligence 5 (1970), 79\u201398.","journal-title":"Machine Intelligence"},{"key":"e_1_2_2_38_1","unstructured":"The Coq development team. 2016. The Coq Proof Assistant Reference Manual. (2016). Version 8.6.  The Coq development team. 2016. The Coq Proof Assistant Reference Manual. (2016). Version 8.6."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_2_40_1","volume-title":"Elementary induction on abstract structures","author":"Moschovakis Yiannis N.","unstructured":"Yiannis N. Moschovakis . 2008. Elementary induction on abstract structures . Dover Publications . Yiannis N. Moschovakis. 2008. Elementary induction on abstract structures. Dover Publications."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-028-4-286"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"e_1_2_2_47_1","volume-title":"PVS: A Prototype Verification System. In CADE\u201911. 748\u2013752","author":"Owre Sam","year":"1992","unstructured":"Sam Owre , John M. Rushby , and Natarajan Shankar . 1992 . PVS: A Prototype Verification System. In CADE\u201911. 748\u2013752 . http:\/\/dl.acm.org\/citation.cfm?id=648230.752639 Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: A Prototype Verification System. In CADE\u201911. 748\u2013752. http:\/\/dl.acm.org\/citation.cfm?id=648230.752639"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Oden Padon Giuliano Losa Mooly Sagiv and Sharon Shoham. 2017. Paxos Made EPR: Decidable Reasoning about Distributed Protocols. In OOPSLA\u201917. To Appear.  Oden Padon Giuliano Losa Mooly Sagiv and Sharon Shoham. 2017. Paxos Made EPR: Decidable Reasoning about Distributed Protocols. In OOPSLA\u201917. To Appear.","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_49_1","volume-title":"Isabelle: The Next 700 Theorem Provers. CoRR cs.LO\/9301106","author":"Paulson Lawrence C.","year":"1993","unstructured":"Lawrence C. Paulson . 1993 . Isabelle: The Next 700 Theorem Provers. CoRR cs.LO\/9301106 (1993). http:\/\/arxiv.org\/abs\/cs.LO\/ 9301106 Lawrence C. Paulson. 1993. Isabelle: The Next 700 Theorem Provers. CoRR cs.LO\/9301106 (1993). http:\/\/arxiv.org\/abs\/cs.LO\/ 9301106"},{"key":"e_1_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Edgar Pek Xiaokang Qiu and Parthasarathy Madhusudan. 2014. Natural proofs for data structure manipulation in C using separation logic. In PLDI\u201914. 440\u2013451. http:\/\/dl.acm.org\/citation.cfm?id=2594291  Edgar Pek Xiaokang Qiu and Parthasarathy Madhusudan. 2014. Natural proofs for data structure manipulation in C using separation logic. In PLDI\u201914. 440\u2013451. http:\/\/dl.acm.org\/citation.cfm?id=2594291","DOI":"10.1145\/2666356.2594325"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958054"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_2_2_54_1","volume-title":"Proceedings of the 3rd Vampire Workshop","author":"Reynolds Andrew","year":"2016","unstructured":"Andrew Reynolds . 2016 . Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. In Vampire@IJCAR 2016 . Proceedings of the 3rd Vampire Workshop , Coimbra, Portugal , July 2, 2016. 1\u201315. Andrew Reynolds. 2016. Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. In Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016. 1\u201315."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_28"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4763-6"},{"key":"e_1_2_2_58_1","first-page":"2","article-title":"E - a brainiac theorem prover","volume":"15","author":"Schulz Stephan","year":"2002","unstructured":"Stephan Schulz . 2002 . E - a brainiac theorem prover . AI Commun. 15 , 2 - 3 (2002), 111\u2013126. http:\/\/content.iospress.com\/ articles\/ai- communications\/aic260 Stephan Schulz. 2002. E - a brainiac theorem prover. AI Commun. 15, 2-3 (2002), 111\u2013126. http:\/\/content.iospress.com\/ articles\/ai- communications\/aic260","journal-title":"AI Commun."},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-23-1-150-161"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_2_2_61_1","volume-title":"Siau-Cheng Khoo, and Wei-Ngan Chin.","author":"Ta Quang-Trung","year":"2016","unstructured":"Quang-Trung Ta , Ton Chanh Le , Siau-Cheng Khoo, and Wei-Ngan Chin. 2016 . Automated Mutual Explicit Induction Proof in Separation Logic. CoRR abs\/1609.00919 (2016). http:\/\/arxiv.org\/abs\/1609.00919 Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2016. Automated Mutual Explicit Induction Proof in Separation Logic. CoRR abs\/1609.00919 (2016). http:\/\/arxiv.org\/abs\/1609.00919"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158098","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158098","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158098","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158098"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158098"],"URL":"https:\/\/doi.org\/10.1145\/3158098","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}