I dokumentet behandlas problemet med att utvidga den positiva Hornklausullogiken genom att införa implikationer i målen som ett verktyg för programstrukturering. Vi tillåter ett mål G, i en klausul G, A A G, + A att vara inte bara en atom utan också en implikation D 3 G (vi ska kalla det ett implikationsmål), där D är en uppsättning av klausuler och G ett mål. Denna utvidgning av språket tillåter lokala definitioner av klausuler i logiska program. I själva verket kan ett indirekt mål D 1 G ses som ett block (D, G), där D är uppsättningen av lokala klausuldeklarationer. I detta dokument definierar vi ett språk med block där regler för statisk räckvidd har valts för lokalt definierade klausuler, liksom för traditionella blockstrukturerade programmeringsspråk. Vi analyserar statiska tillämpningsområderegler, där ett mål endast kan hänvisa till klausuler som definieras i statiskt omgivande block, och vi jämför denna utvidgning med andra förslag i litteraturen. Vi hävdar, på grund av både genomförande och semantiska överväganden, att denna typ av block strukturerade språk är en mycket naturlig förlängning av Horn klausuler när de används som ett programmeringsspråk. Vi visar det genom att definiera en operativ, fixpoint och modell-teoretisk semantik som är förlängningar av standard en, och genom att bevisa deras likvärdighet. Vi visar också att statiska tillämpningsområderegler kan erhållas genom att tolka + som klassiska och + som intuitionistiska konsekvenser med avseende på Herbrands tolkningar.
Likvärdigheten mellan de två modell-teoretiska semantik som presenteras i REF är faktiskt en direkt följd av definitionen av FMod.
Extending Horn Clause Logic with Implication Goals
{'venue': 'Theor. Comput. Sci.', 'journal': 'Theor. Comput. Sci.', 'mag_field_of_study': ['Mathematics', 'Computer Science']}