{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,23]],"date-time":"2024-04-23T23:26:41Z","timestamp":1713914801394},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"4-6","license":[{"start":{"date-parts":[[2010,7,9]],"date-time":"2010-07-09T00:00:00Z","timestamp":1278633600000},"content-version":"unspecified","delay-in-days":8,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic. These reductions are evaluated in the computation of models for FO(FD) theories representing fairness conditions and we provide potential applications of FO(FD).<\/jats:p>","DOI":"10.1017\/s1471068410000293","type":"journal-article","created":{"date-parts":[[2010,7,9]],"date-time":"2010-07-09T12:44:40Z","timestamp":1278679480000},"page":"581-596","source":"Crossref","is-referenced-by-count":13,"title":["FO(FD): Extending classical logic with rule-based fixpoint definitions"],"prefix":"10.1017","volume":"10","author":[{"given":"PING","family":"HOU","sequence":"first","affiliation":[]},{"given":"BROES","family":"DE CAT","sequence":"additional","affiliation":[]},{"given":"MARC","family":"DENECKER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2010,7,9]]},"reference":[{"key":"S1471068410000293_ref13","first-page":"142","volume-title":"LPNMR","author":"Janhunen","year":"2009"},{"key":"S1471068410000293_ref24","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic II","author":"Tseitin","year":"1968"},{"key":"S1471068410000293_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068410000293_ref15","first-page":"134","volume-title":"INAP\/WLP","author":"Kein\u00e4nen","year":"2004"},{"key":"S1471068410000293_ref21","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1995.1053"},{"key":"S1471068410000293_ref16","first-page":"5","volume-title":"TACAS","author":"Liu","year":"1998"},{"key":"S1471068410000293_ref1","volume-title":"Foundations of Databases","author":"Abiteboul","year":"1995"},{"key":"S1471068410000293_ref11","first-page":"182","volume-title":"ATVA","author":"Friedmann","year":"2009"},{"key":"S1471068410000293_ref8","first-page":"170","volume-title":"SAT","author":"Cotton","year":"2006"},{"key":"S1471068410000293_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9118-9"},{"key":"S1471068410000293_ref12","first-page":"27","volume-title":"ICLP","author":"Gupta","year":"2007"},{"key":"S1471068410000293_ref5","volume-title":"Vicious Circles: On the mathematics of Non-Wellfounded Phenomena","author":"Barwise","year":"1996"},{"key":"S1471068410000293_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(86)90032-9"},{"key":"S1471068410000293_ref22","first-page":"434","volume-title":"LPNMR","author":"Syrj\u00e4nen","year":"2001"},{"key":"S1471068410000293_ref2","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","author":"Baader","year":"2003"},{"key":"S1471068410000293_ref3","first-page":"92","volume-title":"LPAR","author":"Baelde","year":"2007"},{"key":"S1471068410000293_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543357"},{"key":"S1471068410000293_ref9","first-page":"703","volume-title":"CL","author":"Denecker","year":"2000"},{"key":"S1471068410000293_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1342991.1342998"},{"key":"S1471068410000293_ref14","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.6.719"},{"key":"S1471068410000293_ref6","first-page":"233","volume-title":"CONCUR","author":"Bradfield","year":"1996"},{"key":"S1471068410000293_ref19","first-page":"321","volume-title":"CAV","author":"Nieuwenhuis","year":"2005"},{"key":"S1471068410000293_ref20","first-page":"59","article-title":"Fixpoint induction and proofs of program properties","volume":"5","author":"Park","year":"1969","journal-title":"Machine Intelligence"},{"key":"S1471068410000293_ref26","first-page":"572","volume-title":"AAAI","author":"Wittocx","year":"2008"},{"key":"S1471068410000293_ref23","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"S1471068410000293_ref25","first-page":"384","volume-title":"ESWC","author":"Vennekens","year":"2009"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068410000293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:32:53Z","timestamp":1556479973000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068410000293\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":26,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["S1471068410000293"],"URL":"https:\/\/doi.org\/10.1017\/s1471068410000293","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7]]}}}