{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T09:13:41Z","timestamp":1673428421572},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2001,12,18]],"date-time":"2001-12-18T00:00:00Z","timestamp":1008633600000},"content-version":"unspecified","delay-in-days":0,"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":[[2002,1]]},"abstract":"<jats:p>In this paper we investigate the theoretical foundation of a new bottom-up semantics for \nlinear logic programs, and more precisely for the fragment of LinLog (Andreoli, 1992) that \nconsists of the language LO (Andreoli &amp; Pareschi, 1991) enriched with the constant <jats:bold>1<\/jats:bold>. We \nuse <jats:italic>constraints<\/jats:italic> to symbolically and finitely represent possibly infinite collections of provable \ngoals. We define a fixpoint semantics based on a new operator in the style of <jats:italic>T<\/jats:italic><jats:sub><jats:italic>P<\/jats:italic><\/jats:sub> working \nover constraints. An application of the fixpoint operator can be computed algorithmically. \nAs sufficient conditions for termination, we show that the fixpoint computation is guaranteed \nto converge for propositional LO. To our knowledge, this is the first attempt to define an \neffective fixpoint semantics for linear logic programs. As an application of our framework, \nwe also present a formal investigation of the relations between LO and Disjunctive Logic \nProgramming (Minker <jats:italic>et al<\/jats:italic>., 1991). Using an approach based on abstract interpretation, we \nshow that DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO. \nWe prove that the resulting abstraction is <jats:italic>correct<\/jats:italic> and <jats:italic>complete<\/jats:italic> (Cousot &amp; Cousot, 1977; \nGiacobazzi &amp; Ranzato, 1997) for an interesting class of LO programs encoding Petri Nets.<\/jats:p>","DOI":"10.1017\/s1471068402001254","type":"journal-article","created":{"date-parts":[[2008,8,14]],"date-time":"2008-08-14T10:46:02Z","timestamp":1218710762000},"page":"85-122","source":"Crossref","is-referenced-by-count":11,"title":["An effective fixpoint semantics for linear logic programs"],"prefix":"10.1017","volume":"2","author":[{"given":"MARCO","family":"BOZZANO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"GIORGIO","family":"DELZANNO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MAURIZIO","family":"MARTELLI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2001,12,18]]},"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\/S1471068402001254","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T19:20:02Z","timestamp":1554060002000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068402001254\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,12,18]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["S1471068402001254"],"URL":"https:\/\/doi.org\/10.1017\/s1471068402001254","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,12,18]]}}}