陳文彬，李福芳，鄒 宇

（廣州大學(xué)a.計(jì)算機(jī)科學(xué)與教育軟件學(xué)院；b.廣東省數(shù)學(xué)教育軟件工程技術(shù)研究中心，廣東 廣州 510006）

穩(wěn)定模的分裂性

陳文彬a，李福芳a，鄒 宇b

（廣州大學(xué)a.計(jì)算機(jī)科學(xué)與教育軟件學(xué)院；b.廣東省數(shù)學(xué)教育軟件工程技術(shù)研究中心，廣東 廣州 510006）

邏輯程序是一些具有正負(fù)子句的規(guī)則集合.基于MOORE提出的自認(rèn)知邏輯的基礎(chǔ)上，GELFOND引進(jìn)了穩(wěn)定模的概念，后來(lái)得到更進(jìn)一步的發(fā)展.在文章中，作者研究了穩(wěn)定模的分裂性質(zhì).這性質(zhì)表明當(dāng)邏輯程序分裂成部分時(shí)候，它的穩(wěn)定模的計(jì)算可以得到簡(jiǎn)化.

穩(wěn)定模；邏輯程序；埃爾布郎模；穩(wěn)定集

0 Introduction

In some cases，a logic program can be split into two parts such that one part does not refer to the predicates defined in the other part.There is a long history about the idea of splitting a logic program into parts.The notation of a stratification is involved with the application of splitting［1］.In a stratified program，by applying the splitting step several times， the intended model can be arrived at.In a locally stratified program［2］，the notation of a stratification has been extended.In a locally stratified program，it may be possible to split a program into infinite parts instead of finite parts.The splitting in the context of“answer set semantic”and several applications have been discussed［3］.

The declarative semantics for a logic program∏can be defined by selecting one of its models as the“canonical”model CM（∏）.Whether an answer toa given query is considered correct is determined by the canonical model.The canonical model is usually selected among the Herbrand models of Q.The Herbrand models are those models whose universe is the set of all ground terms（which do not contain variables）.An Herbrand model is completely determined by the ground atoms that are true in it，and it can be identified with the set of these atoms.

A Herbrand model M of∏is minimal，if no proper subset of M is a model of∏.When a logic program does not contain negation，it has exactly one minimal Herbrand model.A negation-free logic program［5］usually selects the minimal Herbrand model as its canonical model CM（∏）.However，there may be several minimal Herbrand models for logic programs with negation.There has been much work on defining canonical models for logic programs with negation.In the papers（Refs.［1，4-5］），the“stratified”logic programs were introduced，and canonical models were defined for stratified logic programs by an“iterated fixed point”method.Further generalizations can be found in Ref.［2］（“perfect models”）and in Ref.［6］（“well-founded models”）.All these definitions impose some restrictions on the use of negation.GELFOND introduced an approach to negation through stable models［7］，and motivated it by appealing to autoepistemic logic，as developed by MOORE［8］.The theory has been further developed by GELFOND，et al［9］，and also by MAREK and TRUSZCZYNSKI［10-11］.In Ref.［12］，KAMINSKI gives a transformation that embeds logic programs into default logic.In［13-16］，some extends of the stable Model semantic are given.

In this paper，we study the property of stable models when a logic program is split into parts.The property shows how computing the stable model for a logic program can be simplified when the program is split into parts.The splitting process is similar to the one in the context“answer set semantic”［3］.Based on a splitting set，a logic program is split into two parts.Then the union of the stable models of the two parts are the stable models of that logic program.We illustrate the splitting property of stable models by an example.

Paper organization Section 2 gives some background about stable models.Section 3 describes the notion of splitting a logic program and shows the property of stable models for split logic program.An example is given in section 4.We conclude with section 5.

1 Prelim inaries

In the section we follow the definition of Ref.［9］，which defines stability without reference to autoepistemic logic.GELFOND and LIFSCHITZ［9］define a stable model to be one that reproduces itself in a certain three stage transformations，which we call the stability transformation.

The logic programs under consideration are sets of rules of the form

Where A is an atom，and L1，…，Lmare literals（i.e.，atoms or negated atoms），m≥0.Rule（1）is notational variant of the formula

so that any logic programs can be viewed as a set of first order formulas.Accordingly，we can talk about models of a logic program.Every logic program has many different models.

Let∏be a logic program，i.e.，a set of rules of form（1）.We assume that each rule containing variables is replaced by all its ground instance，so that all atoms in∏are ground.（Since∏is not required to be finite，the variables can be eliminated in this way even when the program uses function symbols，and its Herbrand universe is infinite.）

For any set M of atoms from∏，let∏Mbe the program obtained from∏by deleting：

（1）Each rule that has a negative literal?B in its body with B∈M，and

（2）All negative literals in the bodies of the remaining rules.

Clearly，∏Mis negation-free，so that∏Mhas aunique minimal Herbrand model.If this model coincides with M，then we say that M is a stable set of∏.Such sets can be also described as the fixed points of the operator SЦdefined by the condition：for any set M of atoms from∏，SЦ（M）is the minimal Herbrand model of∏M.

Lemma 1 Any stable set of∏is a minimal Herbrand model of∏.

In view of this fact，stable sets can be also called stable models.The proof of lemma 1 is given in Ref.［9］.

2 The splitting property of stable models

In the section we describe the splitting process for logic programs and give the splitting property of stable models.

For any rule of∏，let Pos be the set of positive literals in its body，and let Neg be the set of atoms that represent negative literals in its body.

Definition 1 Let U be a set of literals，we say that U splits∏if for every rule Head←Pos，?（Neg）in∏，Pos∪Neg is contained in U whenever Head∈U.

If U splits∏，then the set of rules in∏whose heads belong to U is the base of∏（relative to U），denoted by bU（∏）.

For any logic program∏，any set U of literals and any subset C of U，eU（∏，C）stands for the program obtained from∏by

（?。ヾeleting each rule Head←Pos，?（Neg）such that Pos∩（UC）≠or Neg∩C≠，

（ⅱ）replacing each remaining rule Head←Pos，?（Neg）by Head←（PosU），?（NegU）.

The theorem below describes the splitting property of stable models.

Theorem 2 Let U be a set of literals that splits a program∏.A consistent set of literals is a stable model for∏if it can be represented in the form C1∪C2，where C1is a stable model for bU（∏）and C2is a stable model for eU（∏U（∏），C1）.

In order to prove that C1is a stable model for bU（∏），we need prove that C1is the minimal Herbrand model of∏1C1where∏1C1denotes bU（∏）by the definition of a stable model.

Given any rule R′∈∏1C1，R′：d←A1，…，Anis reduced from R：d←A1，…，An，?B1，…，?Bmsuch that BiC1for any i.Because BiC1for any i，BiC for any i.Then R′∈∏C.Because C is a stable model，R′is satisfied in C.So R′is satisfied in C1.Then C1is a Herbrand model of∏1C1.

Assume then a subset C3of C1is a model of∏1C1，we show that C3∪C2is also model of∏C.

Given any rule R′∈∏C，R′：d←A1，…，Anis reduced from R：d←A1，…，An，?B1，…，?Bmsuch that BiC for any i.If d∈U，Then R′∈∏1C1.Since C3is a model of∏1C1，R′is satisfied in C3.Then R′is satisfied in C3∪C2.If dU and Aiis true in C3∪C2for any i，Then d is true in C since R′is satisfied in C.Thus d∈C.since dU，d∈C2.Hence R′is satisfied in C3∪C2.Thus C3∪C2is a Herbrand model of∏C.Because C is the minimal Herbrand model of∏C，C＝C3∪C2.Hence C3＝C1.Thus C1is the minimal Herbrand model of∏1C1.So C1is a stable model for bU（∏）.

Now we show that C2is a stable model for eU（∏U（∏），C1）.Let∏2denote eU（∏U（∏），C1）.It suffices to show that C2is the minimal Herbrand model of∏2C2.We prove first that C2is a Herbrand model of∏2C2.

Assume that R′is a rule of∏2C2and R′：d←A1，…，Anis reduced from R：d←A1，…，An，?B1，…，?Bmsuch that BiC2for any i.Since R∈∏2，BiU for any i.Thus Bidoesn’t belong to C1.Hence BiC for any i.So R′∈∏C.Since C is a stable model for∏，R′is satisfied in C.Hence if Aiis true in C2for any i，then d is true in C.Then d∈C.Since dU，d∈C2.Thus R′is satisfied in C2.So C2is a Herbrand model of∏2C2.

Furthermore we prove that C2is minimal model.Suppose that a subset C4of C2is a model of∏2C2.We show that C4∪C1is also model of∏C.

Given any rule R′∈∏C，R′：d←A1，…，Anis reduced from R：d←A1，…，An，?B1，…，?Bmsuch that BiC for any i.If d∈U，then R′∈∏1C1.Since C1is a model of∏1C1，R′is satisfied in C1.Then R′is true in C4∪C1.If dU and A1，…，Anare true in C4∪C1，then we suppose that A1，…，Ahbelong to C4and other Aibelong to C1.Then R″：d←A1，…，Ahbelong to∏2.Thus R″belongs to∏2C2.Since C4is a model of∏2C2，R″is satisfied in C4.So d is true in C4.Thus R′is satisfied in C4∪C1.So C4∪C1is a model of∏C.Because C is the minimal Herbrand model of∏C，C＝C4∪C1.Hence C4＝C2.Thus C2is the minimal Herbrand model of∏2C2.So C2is a stable model for eU（∏U（∏），C1）.

Given any rule R′∈∏C，R′：d←A1，…，Anis reduced from R：d←A1，…，An，?B1，…，?Bmsuch that BiC for any i.If d∈U，then R′∈∏1C1.Since C1is a model of∏1C1，R′is satisfied in C1.Then R′is true in C1∪C2.If dU and A1，…，Anare true in C1∪C2，then we suppose that A1，…，Ahbelong to C2and other Aibelongs to C1.Then R″：d←A1，…，Ahbelong to∏2.Thus R″belongs to∏2C2.Since C2is a model of∏2C2，R″is satisfied in C2.So d is true in C2.Thus R′is satisfied in C2∪C1.So C2∪C1is a model of∏C.

If a subset D of C is a model of∏C，then D∩U is a model of∏1C1by the proof of the first part.So D∩U＝C1.Similarly，DU＝C2.Then D＝C1∪C2. Hence C is the minimal Herbrand model of∏C.So C is a stable model for∏.

3 Exam ples

The next example illustrates the splitting property of stable models.Consider the logic program consisting of the three rules below.

Let∏be（2）with the third rule replaced by its ground instance：

It has exactly one stable model C1，which is｛P（1，2），P（2，1）｝.Then we can obtain eU（∏U（∏），C1）below：

It has two stable models：C21＝｛Q（1）｝，C22＝｛Q（2）｝.So∏has two stable models：

4 Conclusion

We discuss the idea of splitting a logic program in the context of the stable model semantics.The splitting property of stable models is showed in this paper.The property shows how computing the stable model for a logic program can be simplified when the program is split into parts.The splitting process is similar to the one in the context“answer set semantic”［7］.Based on a splitting set，a logic program is split into two parts.Then the union of the stable models of the two parts are the stable models of that logic program.We illustrate the splitting property of stable models by an example.

Acknow ledgements

We would like to thank the anonymous referees for their careful reading of the manuscripts and many useful suggestions.

［1］ APT K R，BLAIR，WALKER A.Towards a theory of declarative knowledge［M］∥MINKER J（ed.），F(xiàn)oundations of Deductive Data-bases and Logic Programming.Los Altos：Morgan Kaufmann Publishers，1988：89-148.

［2］ PRZYMUSINSKI T.On the declarative semantics of stratified deductive databases and logic programs［M］∥MINKER J（ed.），F(xiàn)oundations of Deductive Databases and Logic Programming.Los Altos：Morgan Kaufmann Publishers，1988：193-216.

建設(shè)榆林特色生態(tài)名市，是榆林市“十二五”規(guī)劃確立的重要內(nèi)容，榆陽(yáng)區(qū)做為這一規(guī)劃施行的主陣地，科學(xué)規(guī)劃，分類(lèi)指導(dǎo)，數(shù)十年堅(jiān)持“南治土、北治沙”，取得了舉世矚目的成績(jī)。

［3］ LIFSCHTI V，TURNER V.Splitting a logic program［M］∥HENTENRYCK P V（ed.），Proc.Eleventh Int’l Conf.on Logic Programming，1994，23-37.

［4］ CHANDRA A，HAREL D.Horn clause queries and generalizations［J］.Logic Program，1985，1：1-15.

［5］ VAN GELDER A.Negation as failure using tight derivations for general logic programs［M］∥MINKER J（ed.），F(xiàn)oundations of Deductive Databases and Logic Programming.Los Altos：Morgan Kaufmann Publishers，1988：193-216.

［6］ VAN GELDER A，ROSS K，SCHLIPF J S.Unfounded sets and well-founded semantics for general logic programs［C］∥Proc.Seventh Symp.On Principles of Database Systems，1988：221-230.

［7］ GELFOND M.On stratified autoepistemic theories［C］∥Proc.AAAI，1987.

［8］ MOORE R.Semantical considerations on nonmonotomic logic［J］.Artif Intell，1985，28：75-94.

［9］ GELFOND M，LIFSCHTIZ V.The stable model semantics for logic programming［C］∥In Fifth Int’l Conf.Symp.on Logic Programming，Seattle，1988：1070-1080.

［10］MAREK A，TRUSZCZYNSKI M.Autoepistemic logic［R］.University of Kentucky，1988.

［11］MAREK W.Stable theories in autoepistemic logic［R］.University of Kentucky，1986.

［12］KAMINSKI M.A note on the stable model semantics for logic programs［J］.Artif Intell，1997，96（2）：467-479.

［13］SIMONS P，NIEMELA I，SOININEN T.Extending and implementing the stable model semantics［J］.Artif Intell，2002，138（1/2）：181-234.

［14］JANHUNEN T，OIKARINEN E.Testing the equivalence of logic programs under stable model semantics［J］.JELIA，2002，2424：493-504.

［15］PEREIRA L M，PINTO A M.Revised stable models：A semantics for logic programs［J］.LNAI，2005，3808：29-42.

［16］BENHAMOU B，SIEGEL P.A new semantics for logic programs capturing and extending the stable model semantics［J］.IEEE Internat Confer Tool Artif Intell，2012，8345（11）：572-579.

【責(zé)任編輯：陳 鋼】

The sp litting property of stable models

CHEN W en-bina，LI Fu-fanga，ZOU Yub
（a.School of Computer Science and Educational Software，b.Guangdong Prouincial Engineering Technology Research Center for Mathematical Educational Software，Guangzhou University，Guangzhou 510006，China）

A general logic program is a set of rules that have both positive and negative subgoals.GELFOND introduced an approach to negation through stable models，and motivated it by appealing to autoepistemic logic，as developed by MOORE.The theory has been further developed by GELFOND，et al，and also by MAREK and TRUSZCZYNSKI.In this paper we study the splitting property of stable models.The property shows how computing the stable model for a logic program can be simplified when the program is split into parts.

stable models；logic programs；Herbrand model；stable set

ET 471 Document code：A

TP 18

A

1671-4229（2016）01-0013-05

Received date：2015-12-15； Revised date：2015-12-25

Foundation items：National Science Foundation of China（NSFC）under Grant No.11271097.Natural Science Foundation of China under Grant No.61472092；Guangdong Provincial Science and Technology Plan Project under Grant No.2013B010401037；and Guangzhou Municipal High School Science Research Fund under Grant No.120142131.

Biography：CHEN Wen-bin（1975-），male，associate professor.Ph.D.E-mail：cwb2011＠gzhu.edu.cn.