{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T14:46:31Z","timestamp":1776350791597,"version":"3.51.2"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2026,4,30]]},"abstract":"<jats:p>We consider a class of formula equations in first-order logic, Horn formula equations, which are defined by a syntactic restriction on the occurrences of predicate variables. Horn formula equations play an important role in many applications in computer science. We state and prove a fixed-point theorem for Horn formula equations in first-order logic with a least fixed-point operator. Our fixed-point theorem is abstract in the sense that it applies to an abstract semantics which generalises standard semantics. We describe several corollaries of this fixed-point theorem in various areas of computational logic, ranging from the logical foundations of program verification to inductive theorem proving.<\/jats:p>","DOI":"10.1145\/3779416","type":"journal-article","created":{"date-parts":[[2025,12,15]],"date-time":"2025-12-15T18:28:24Z","timestamp":1765823304000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["An Abstract Fixed-Point Theorem for Horn Formula Equations"],"prefix":"10.1145","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6461-5982","authenticated-orcid":false,"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry, TU Wien, Wien, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2471-9407","authenticated-orcid":false,"given":"Johannes","family":"Kloibhofer","sequence":"additional","affiliation":[{"name":"Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,20]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448035"},{"key":"e_1_3_3_3_2","volume-title":"Rudiments of Calculus","author":"Arnold A.","year":"2001","unstructured":"A. Arnold and D. Niwinski. 2001. Rudiments of Calculus. Elsevier Science."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00106-9"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01190829"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_28"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01976313"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01982011"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18170-9_151"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158099"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80065-2"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005722130532"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1998-3612"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2015.01.002"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exv059"},{"key":"e_1_3_3_19_2","volume-title":"A Mathematical Introduction to Logic","author":"Enderton Herbert B.","year":"2001","unstructured":"Herbert B. Enderton. 2001. A Mathematical Introduction to Logic (2nd ed.). Academic Press."},{"key":"e_1_3_3_20_2","volume-title":"Quantifier Elimination in Second-Order Predicate Logic","author":"Engel T.","year":"1996","unstructured":"T. Engel. 1996. Quantifier Elimination in Second-Order Predicate Logic. Diplomarbeit. Fachbereich Informatik, Univ. des Saarlandes, Saarbr\u00fccken, Germany."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4_20"},{"key":"e_1_3_3_22_2","first-page":"35","article-title":"Quantifier elimination in second order predicate logic","volume":"7","author":"Gabbay Dov","year":"1992","unstructured":"Dov Gabbay and Hans J\u00fcrgen Ohlbach. 1992. Quantifier elimination in second order predicate logic. South African Computer Journal 7 (1992), 35\u201343.","journal-title":"South African Computer Journal"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/1816959"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24771-5_13"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020821"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.169.5"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC49474.2019.00010"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266967"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.344.5"},{"key":"e_1_3_3_30_2","first-page":"59","volume-title":"Proceedings of the 2nd Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE)","author":"Hetzl Stefan","year":"2021","unstructured":"Stefan Hetzl and Johannes Kloibhofer. 2021. An abstract fixed-point theorem for Horn formula equations (abstract). In Proceedings of the 2nd Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE). CEUR-WS.org, 59\u201360."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exz033"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_36"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2109.03988"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3614319"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80029-8"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571262"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_14"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_3_42_2","unstructured":"Johannes Kloibhofer. 2020. A Fixed-Point Theorem for Horn Formula Equations. Master\u2019s Thesis. TU Wien Austria."},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_20"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571199"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_25"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/1024196"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00297246"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80013-6"},{"key":"e_1_3_3_49_2","unstructured":"Kenneth L. McMillan and Andrey Rybalchenko. 2012. Solving Constrained Horn Clauses Using Interpolation. Technical Report Microsoft Research MSR-TR-2013-06."},{"key":"e_1_3_3_50_2","volume-title":"Elementary Induction on Abstract Structures","author":"Moschovakis Yiannis N.","year":"1974","unstructured":"Yiannis N. Moschovakis. 1974. Elementary Induction on Abstract Structures. North Holland."},{"key":"e_1_3_3_51_2","first-page":"307","volume-title":"A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory. Studies in Fuzziness and Soft Computing","author":"Nonnengart Andreas","year":"1998","unstructured":"Andreas Nonnengart and Andrzej Sza\u0142as. 1998. A Fixpoint Approach to Second-Order Quantifier Elimination with Applications to Correspondence Theory. Studies in Fuzziness and Soft Computing, Vol. 24. Springer, 307\u2013328."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61511-3_77"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2006.03.003"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSC.2007.01.002"},{"key":"e_1_3_3_55_2","volume-title":"Boolean Functions and Equations","author":"Rudeanu Sergiu","year":"1974","unstructured":"Sergiu Rudeanu. 1974. Boolean Functions and Equations. North-Holland."},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"e_1_3_3_57_2","volume-title":"Vorlesungen \u00dcber Die Algebra Der Logik","author":"Schr\u00f6der Ernst","year":"1890","unstructured":"Ernst Schr\u00f6der. 1890. Vorlesungen \u00dcber Die Algebra Der Logik. Vol. 1. Teubner."},{"key":"e_1_3_3_58_2","volume-title":"Metric Affine Geometry","author":"Snapper Ernst","year":"1971","unstructured":"Ernst Snapper and Robert J. Troyer. 1971. Metric Affine Geometry. Academic Press."},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394766"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498725"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_30"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"},{"key":"e_1_3_3_64_2","first-page":"82","volume-title":"Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE \u201917)","author":"Wernhard Christoph","year":"2017","unstructured":"Christoph Wernhard. 2017. Approximating resultants of existential second-order quantifier elimination upon universal relational first-order formulas. In Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE \u201917), 82\u201398."},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_19"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/151145"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779416","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T13:51:36Z","timestamp":1776347496000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779416"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,20]]},"references-count":65,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4,30]]}},"alternative-id":["10.1145\/3779416"],"URL":"https:\/\/doi.org\/10.1145\/3779416","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,20]]},"assertion":[{"value":"2022-02-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-29","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-03-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}