{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:34:37Z","timestamp":1774060477476,"version":"3.50.1"},"reference-count":23,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,4,20]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present formula equations\u2014first-order formulas with unknowns standing for predicates\u2014as a general formalism for treating certain questions in logic and computer science, like the Aufl\u00f6sungsproblem and loop invariant generation. In the case of the language of affine terms over $\\mathbb{Q}$, we translate a quantifier-free formula equation into an equivalent statement about affine spaces over $\\mathbb{Q}$, which can then be decided by an iteration procedure.<\/jats:p>","DOI":"10.1093\/logcom\/exz033","type":"journal-article","created":{"date-parts":[[2019,11,11]],"date-time":"2019-11-11T12:10:52Z","timestamp":1573474252000},"page":"697-714","source":"Crossref","is-referenced-by-count":2,"title":["Decidability of affine solution problems"],"prefix":"10.1093","volume":"30","author":[{"given":"Stefan","family":"Hetzl","sequence":"first","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry, Faculty of Mathematics and Geoinformation, TU Wien, 1040 Vienna, Austria"}]},{"given":"Sebastian","family":"Zivota","sequence":"first","affiliation":[{"name":"Institute of Discrete Mathematics and Geometry, Faculty of Mathematics and Geoinformation, TU Wien, 1040 Vienna, Austria"}]}],"member":"286","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"2020050200390836100_ref1","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/BF01448035","article-title":"Untersuchungen \u00fcber das Eliminationsproblem der mathematischen Logik","volume":"110","author":"Ackermann","year":"1935","journal-title":"Mathematische Annalen"},{"key":"2020050200390836100_ref2","doi-asserted-by":"crossref","DOI":"10.25368\/2022.74","article-title":"On the complexity of Boolean unification","volume-title":"LTCS-Report LTCS-97-03","author":"Baader","year":"1997"},{"key":"2020050200390836100_ref3","first-page":"24","volume-title":"Horn Clause Solvers for Program Verification","author":"Bj\u00f8rner","year":"2015"},{"key":"2020050200390836100_ref4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/S0747-7171(87)80065-2","article-title":"Embedding Boolean expressions into logic programming","volume":"4","author":"B\u00fcttner","year":"1987","journal-title":"Journal of Symbolic Computation"},{"key":"2020050200390836100_ref5","doi-asserted-by":"crossref","first-page":"665","DOI":"10.1016\/j.apal.2015.01.002","article-title":"Inductive theorem proving based on tree grammars","volume":"166","author":"Eberhard","year":"2015","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020050200390836100_ref6","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1093\/logcom\/exv059","article-title":"Boolean unification with predicates","volume":"27","author":"Eberhard","year":"2017","journal-title":"Journal of Logic and Computation"},{"key":"2020050200390836100_ref7","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1090\/S0002-9939-1974-0325378-3","article-title":"The undecidability of theories of groupoids with an extra predicate","volume":"42","author":"Garfunkel","year":"1974","journal-title":"Proceedings of the American Mathematical Society"},{"key":"2020050200390836100_ref8","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-319-08587-6_17","article-title":"Introducing quantified cuts in logic with equality","volume-title":"Automated Reasoning\u20147th International Joint Conference, IJCAR","author":"Hetzl","year":"2014"},{"key":"2020050200390836100_ref9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2014.05.018","article-title":"Algorithmic introduction of quantified cuts","volume":"549","author":"Hetzl","year":"2014","journal-title":"Theoretical Computer Science"},{"key":"2020050200390836100_ref10","article-title":"Some observations on the logical foundations of inductive theorem proving","volume":"13","author":"Hetzl","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"2020050200390836100_ref11","volume-title":"A Shorter Model Theory","author":"Hodges","year":"1997"},{"key":"2020050200390836100_ref12","first-page":"530","article-title":"Polynomial invariants for affine programs","volume-title":"33rd Annual Symposium on Logic in Computer Science (LICS)","author":"Hrushovski","year":"2018"},{"key":"2020050200390836100_ref13","first-page":"299","article-title":"Constraint query languages","volume-title":"Proceedings of the Ninth Symposium on Principles of Database Systems (PODS)","author":"Kanellakis","year":"1990"},{"key":"2020050200390836100_ref14","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1006\/jcss.1995.1051","article-title":"Constraint query languages","volume":"51","author":"Kanellakis","year":"1995","journal-title":"Journal of Computer and System Sciences"},{"key":"2020050200390836100_ref15","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00268497","article-title":"Affine relationships among variables of a program","volume":"6","author":"Karr","year":"1976","journal-title":"Acta Informatica"},{"key":"2020050200390836100_ref16","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF00297246","article-title":"Unification in Boolean rings","volume":"4","author":"Martin","year":"1988","journal-title":"Journal of Automated Reasoning"},{"key":"2020050200390836100_ref17","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/S0747-7171(89)80013-6","article-title":"Boolean unification\u2014the story so far","volume":"7","author":"Martin","year":"1989","journal-title":"Journal of Symbolic Computation"},{"key":"2020050200390836100_ref18","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/s00236-018-0324-y","article-title":"On the decidability of the existence of polyhedral invariants in transition systems","volume":"56","author":"Monniaux","year":"2019","journal-title":"Acta Informatica"},{"key":"2020050200390836100_ref19","first-page":"330","article-title":"Precise interprocedural analysis through linear algebra","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201804","author":"M\u00fcller-Olm","year":"2004"},{"key":"2020050200390836100_ref20","volume-title":"Vorlesungen \u00fcber Die Algebra der Logik","author":"Schr\u00f6der"},{"key":"2020050200390836100_ref21","volume-title":"Metric Affine Geometry","author":"Snapper","year":"1971"},{"key":"2020050200390836100_ref22","first-page":"333","article-title":"The Boolean solution problem from the perspective of predicate logic","volume-title":"11th International Symposium on Frontiers of Combining Systems, FroCoS 2017","author":"Wernhard","year":"2017"},{"key":"2020050200390836100_ref23","first-page":"abs\/1706.08329","article-title":"The Boolean solution problem from the perspective of predicate logic\u2014extended version","author":"Wernhard","year":"2017","journal-title":"Clinical Orthopaedics and Related Research"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/3\/697\/33154057\/exz033.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/3\/697\/33154057\/exz033.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,4]],"date-time":"2022-10-04T08:44:19Z","timestamp":1664873059000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/3\/697\/5688170"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":23,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2019,1,2]]},"published-print":{"date-parts":[[2020,4,20]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz033","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,4]]},"published":{"date-parts":[[2019,1,2]]}}}