Eliminating Disjunction from Propositional Logic Programs under Stable Model Preservation
Eliminating Disjunction from Propositional Logic
Programs under Stable Model Preservation
Thomas Eiter,Michael Fink,Hans Tompits,and Stefan Woltran
Institut f¨u r Informationssysteme184/3,Technische Universit¨a t Wien,
Favoritenstra?e9-11,A-1040Vienna,Austria
eiter,michael,tompits,stefan@kr.tuwien.ac.at Abstract.In general,disjunction is considered to add expressive power to propo-
sitional logic programs under stable model semantics,and to enlarge the range of
problems which can be expressed.However,from a semantical point of view,
disjunction is often not really needed,in that an equivalent program without dis-
junction can be given.We thus consider the question,given a disjunctive logic
program,does there exist an equivalent normal(i.e.,disjunction-free)logic
program?In fact,we consider this issue for different notions of equivalence,
namely for ordinary equivalence(regarding the collections of all stable models
of the programs)as well as for the more restrictive notions of strong and uniform
equivalence.We resolve the issue for propositional programs,and present a sim-
ple,appealing semantic criterion for the programs from which all disjunctions can
be eliminated under strong equivalence;testing this criterion is coNP-complete.
We also show that under ordinary and uniform equivalence,this elimination is
always possible.In all cases,there are constructive methods to achieve this.Our
results extend and complement recent results on simplifying logic programs un-
der different notions of equivalence,and add to the foundations of improving
implementations of Answer Set Solvers.
1Introduction
Disjunctive logic programming is an extension to normal logic programming which is generally considered to add expressive power to logic programs under stable model se-mantics,and to enlarge the range of problems which can be expressed.This view is supported by results on the expressiveness of disjunctive logic programs(DLPs)over ?nite structures,which show that properties at the second level of the Polynomial Hi-erarchy(PH)can be expressed by inference from function-free(Datalog)DLPs[11], while by normal logic programs only properties at the?rst level can be expressed[28]. However,from a semantical point of view,disjunction is often not really needed,in that an equivalent normal logic program(NLP,i.e.,without disjunction)can be given.For example,in[10],it was shown that in the presence of functions symbols,DLPs have over Herbrand models the same expressive power as NLPs,namely.
With the rise of Answer Set Programming as a program solving paradigm,in which solutions are computed in the answer sets resp.stable models of a logic program,at-tention has been directed to the expressiveness of logic programs in terms of the whole
152Thomas Eiter et al.
collection of their answer sets per se rather than their intersection(resp.union)as in cautious and brave reasoning,respectively),cf.[20];related to this is preliminary work on the expressiveness of formalisms such as default logic and circumscription[13,19].
In particular,equivalence of logic programs in terms of their collections of stable models has been considered,as well as the re?ned notions of strong equivalence,cf. [16,29,30,24,17,4],and uniform equivalence[7,8,25],which dates back to[27,18]. Two DLPs and are strongly equivalent(resp.,uniformly equivalent),if,for any set of rules(resp.,set of atoms),the programs and are equivalent
under the stable semantics,i.e.,have the same set of stable models.
Strong and uniform equivalence can be utilized for program optimization,cf.[30, 22,8],taking into account possible incompleteness of a program,where not all rules are known at the time of optimization,respectively varying input data given by atomic facts are respected.This is in particular helpful for optimizing components which are embedded into a more complex logic program.Note that as recently discussed by Pearce and Valverde[25],uniform and strong equivalence are essentially the only concepts of equivalence obtained by varying the logical form of the program extensions.
A natural issue in this context is the expressiveness of disjunction in rule heads, i.e.,whether it really adds expressive power.This is indeed the case,as can be seen on the simple example of the program:This program is not strongly equivalent to any normal logic program(cf.[30]).However,as easily seen is equivalent to the NLP since for both the stable models are and,and furthermore is also uniformly equivalent to (this is immediate from the result that rewriting a head-cycle free program to a normal logic program by standard shifting preserves uniform equivalence[7]).On the other hand,the enriched program is strongly equivalent to the program.
This raises the question of a criterion which tells when disjunctions can be elimi-nated,and a method for deciding,given a disjunctive logic program,does there exist an equivalent normal(i.e.,disjunction-free)program?We study this issue for propo-sitional programs,on which we focus here,and make the following contributions:
–We present a simple,appealing semantic characterization of the programs from which all disjunctions can be eliminated under strong equivalence.The charac-terization is based on the strong-equivalence models(SE-models)[29,30]which rephrase models in the more general logic of here-and-there[16]in logic program-ming terms.In fact,we show that this property holds for a program if and only if the collection of SE-models of is closed under here-intersection,i.e., whenever and are SE-models of,then also is an SE-model of.In more familiar terms,this condition is equivalent to the prop-erty that for each classical model of,the Gelfond-Lifschitz reduct of is semantically Horn if models not contained in are disregarded.
–We further show that under ordinary and uniform equivalence,this elimination is always possible.In all three cases,we obtain a constructive method to rewrite a DLP to an equivalent normal logic program.In general,the rewriting will be of exponential size(if it exists),but this will be unavoidable in practice.
–Finally,we show that testing whether for a given propositional DLP a strongly equivalent NLP exists is coNP-complete.
Eliminating Disjunction from Propositional Logic Programs153 Our results extend and complement recent results on simplifying logic programs un-der different notions of equivalence,cf.[22,30,8].They might be utilized for deciding whether a given disjunctive problem representation for a system such as such as DLV [6]or GnT[14]can,in principle,be replaced by an equivalent non-disjunctive repre-sentation,as well as for(automated)rewriting of disjunctive problem representations.
2Preliminaries
We deal with propositional disjunctive logic programs,containing rules of form
,where all are atoms from a?nite set of propositional atoms,, and denotes default negation.The head of is the set=,and the body of is the set=...,...,.We also use =and=.Moreover,for a set of atoms ,denotes.
A rule is normal,if;positive,if;and Horn,if it is normal and positive.If and,then is a constraint;if,is a fact, written as if,and as otherwise.
A disjunctive logic program(DLP)is a?nite set of rules.It is a normal logic program(NLP)(resp.,positive,Horn),if every is normal(resp.,positive,Horn).
We recall the stable model semantics for DLPs[12,26].Let be an interpretation, i.e.,a subset of.Then,satis?es a rule,denoted,iff whenever
,where iff for some,and iff(i)each
is true in,i.e.,,and(ii)each is false in,i.e.,. Furthermore,is a model of a program,denoted,iff,for all.
The reduct,,of a rule relative to a set of atoms is the positive rule such that and if,and is void otherwise.The Gelfond-Lifschitz reduct of a program is the positive program. An interpretation is a stable model of a program iff is a minimal model(under set inclusion)of.By we denote the set of all stable models of.
Lemma1.Let be a DLP and.Then,implies. The result is seen by the observation that implies.Thus, implies.In particular,for,implies,for any.
Several notions of equivalence for logic programs have been considered in the liter-ature(see,e.g.,[16,18,27]).Under stable semantics,two DLPs and are regarded as equivalent,denoted,iff.The more restrictive forms of strong equivalence[16]and uniform equivalence[27,18]are as follows:
De?nition1.Let and be two DLPs.Then,
(i)and are strongly equivalent,denoted,iff,for any set of rules,the
programs and are equivalent,i.e.,.
(ii)and are uniformly equivalent,denoted,iff,for any set of non-disjunctive facts,and are equivalent,i.e.,.
154Thomas Eiter et al.
Obviously,implies but not vice versa.Both notions of equivalence, however,enjoy interesting semantical characterizations.As shown in[16],strong equiv-alence is closely related to the non-classical logic of here-and-there,which was adapted to logic-programming terms by Turner[29,30]:
De?nition2.A pair with such that is called an SE-interpretation(over).By we denote the of all SE-interpretations over.An SE-interpretation is an SE-model of a DLP,if and.By we denote the set of all SE-models of.
Proposition1([29,30]).For every DLP and,iff.
SE-models also can be used to determine the stable models of a program. Proposition2([23,16]).Let be a DLP.Then,iff
and,for each,.
Recently,the following pendant to SE-models,characterizing uniform equivalence for(?nite)logic programs has been de?ned[7].
De?nition3.Let be a DLP and.Then,is UE-model of iff,for every,it holds that implies.By we denote the set of all UE-models of.
Proposition3([7];cf.also[25]).For any DLP and,iff.
This test can be reformulated as follows.
Proposition4.For DLPs and,iff and. Proof.From Proposition3,iff and. Clearly,holds for any DLP,which immediately gives the only-if direction.For the if direction,suppose.Hence,there exists an SE-interpretation ,such that either(i)and;or(ii)
and.For(i),we have two cases,by de?nition of UE-models. First,.But then,cannot hold.Second,there exists a set with such that.But since ,hence cannot hold.The argument for(ii)is analogous.
As a?nal result here,we characterize the set of SE-models of a disjunctive rule. Proposition5.Let be a disjunctive rule,and an SE-interpretation.Then, holds iff one of the following conditions is satis?ed:(i); (ii);or(iii)and.
Proof.By de?nition,iff,and.The former holds iff ,,or.The latter holds iff,, or.Hence,iff or
(1)
Eliminating Disjunction from Propositional Logic Programs155
Clearly,implies and,furthermore,implies .From this,it is easily veri?ed that satis?es(1)iff either,
(i.e.,(i)),or jointly and(i.e.,(iii)),holds.Hence, we have that iff either,,(i),or(iii)holds. Finally,or holds exactly iff(i.e.,(ii))holds.
3Strong Equivalence
We start with some informal discussion.Consider the following logic programs,each of them having as its only disjunctive rule.
Let us?rst compute the SE-models(over)of these programs:1
A good approximation to derive corresponding strongly equivalent normal logic pro-grams is to replace by the rules,i.e.,by the usual shifting technique.It is left to the reader to verify that this replacement works for, ,,and,but not for,,,,and.In fact,for the latter programs this replacement yields an additional SE-model.In some of these cases we can circumvent this problem by adding further rules.As is easily seen,adding to, ,and,respectively,solves this problem,since,and,for each ,holds().For and this does not work.As we will see soon,there is no normal logic program strongly equivalent to or.
Let us have a closer look at the difference between the SE-models of a disjunctive rule and its corresponding shifting rules.
Proposition6.For a disjunctive rule,,de?ne
;and
Then,.
156Thomas Eiter et al.
Proof.In what follows let denote that rule in with.
Clearly,we have and.In particular,the former relation can be seen by the fact that,for each,holds,since and.
It remains to show.Therefore,let
and suppose.We show that.Towards a contradiction, suppose.Since,we get by Proposition5that, ,and either or.We have two cases.
First,if,i.e.,,this clearly contradicts. Otherwise,if,we have,and we get,otherwise .Let and consider the rule.Obviously,. Moreover,we have.But then,,i.e.,, yields,and thus contradicts.
In other words,contains all SE-interpretations such that with and.Thus,and are disjoint,although,for each
,holds.
Hence,if we have a disjunctive program with a disjunctive rule;we can replace by but this may yield additional SE-models from.(The same observation can be found in[7],see Theorem4.3).In particular,this is the case if
.So,in addition to,we add the following rules which under certain circumstances eliminate all elements from but none from. Proposition7.For any sets,,de?ne the set of rules
Then,is SE-model of iff one of the following conditions holds:(1);(2);(3);or(4)and. Proof.Let and the corresponding rule in with.By Propo-sition5,iff one of the following conditions hold:(i)
(i.e.,);(ii)(i.e.,either or);or(iii)
and(i.e.,and).For any two rules,we have .Thus,iff either(ii),or,for any, (i)or(iii)holds.For the latter relations consider two cases.If,the relation holds iff for each,i.e.,for each.Hence,the relation holds iff.If and then from(iii)for each.Hence, has then to hold.
The rules play a central role and will be subsequently applied in several ways.However,we mention that may contain redundant rules,for instance if we have.It can be shown that then,which reduces the number of rules.However,for technical reasons we subsequently do not pay attention to this potential optimization.
De?nition4(here-intersection).2For any pair of SE-interpretations,and of,their here-intersection is the SE-interpretation.
Eliminating Disjunction from Propositional Logic Programs157 Recall our examples.The difference between and on the one side,and, ,and on the other side,is captured by the following property.
De?nition5.For any logic program,we say that is closed under here-intersection iff satis?es this property.
Lemma2.Each normal LP is closed under here-intersection.
Proof.Since is normal,is Horn.Then,and immediately implies since,each Horn program,satis?es the intersection property: and implies.
This leads us directly to our?rst central theorem.
Theorem1.Let be a DLP over.Then,there exists a NLP over,such that and are strongly equivalent iff is closed under here-intersection.
Proof.The only-if direction is immediate by Lemma2.For the if direction,assume is closed under here-intersection,let be disjunctive,let,and consider the logic program
with,
where
. Intuitively,collects,for each which is also SE-model of,the minimal SE-models of above(with?xed).Note that by de?nition of, for any,but implies existence of an with such that,since for,
holds(again by de?nition of).
We proceed with the proof and show.Clearly,if this holds,the above transformation sequentially applied to all disjunctive rules in yields a normal logic program strongly equivalent to.First observe that,by Proposition6,we have
The strategy for the remainder of the proof is as follows.We?rst show that
.Then,it remains to show.
We show.Let.If,we immediately have .Otherwise,.From above we know that then there exists
158Thomas Eiter et al.
a triple with.Thus,we have.We now show that.Assume the contrary,i.e.,. Then,by Proposition7one of the following conditions has to hold:(i),(ii) ,(iii),or(iv)and.(i)does not hold since we have ;(ii)since,which follows from;(iii+iv)do not hold trivially.Contradiction.
It remains to show that,i.e.,that
holds.Clearly,if is empty we are done.Hence,suppose.We show that, for each and each,holds. Towards a contradiction,let,,and suppose
.On the one hand,from,we have,which implies that(a);(b);and(c)
hold.On the other hand,by Proposition7,satis?es the following conditions for being a counter SE-model of:(1),(2),(3),and(4) or.
By assumption,.Hence,and.Moreover, by(3),holds.By Lemma1,we get and,and from(b) we get,and thus.Hence,and .Now is closed under here-intersection yielding,and
.We use(4)to distinguish between the following two cases.
:By(c),,and thus.On the other hand,from(1), we have.This implies.Hence,we have. Together with(a)and this clearly contradicts ,since is not minimal anymore.
:We have a similar argumentation.By(4),holds,yielding .Moreover,by(2)and by(c)hold.Thus,. Again,we have,and by(a)and,this contradicts.
Let us apply the construction of as used in the proof to the examples discussed in the beginning of the section(except and which are not closed under here-intersection).They all have as their only disjunctive rule.Hence, .Consider now.Clearly,if,is just replaced by.This applies to.For programs,
,and by the SE-models of the respective programs we get
and.Thus in and,exchange by, with(under assumption).This goes well conform from our informal analysis in the beginning of the section.Finally,for,we use instead of,yielding the following normal program
which is obviously strongly equivalent to.The latter has as its only SE-model and thus is strongly equivalent to.
4Uniform Equivalence
The intuitive problems in constructing a uniform equivalent normal logic program from a given disjunctive program are very similar to those observed in the case of strong
Eliminating Disjunction from Propositional Logic Programs159 equivalence.Consider a program having as its only disjunctive rule.Again,a good starting point is to replace by its corresponding shifting rules.But now,an SE-model from only comes into play,iff it is also UE-model of the rest program, i.e.,for each with,implies.Thus,if we want to eliminate such an SE-model,the problem of eliminating further SE-models, which should be retained,is less complicated compared to the case of strong equiva-lence.Roughly speaking,because of this difference we are always able to construct a uniformly equivalent normal program.For instance,all our example programs–except are uniformly equivalent to the program resulting from with replaced by.,however,matches exactly the case where is UE-model of the rest program.Adding rules as or(or both of them)circumvents the problem.Hence,in some(but less)cases we again have to add further rules,but as is seen in proof below,the difference to the construction of is very subtle.
Theorem2.For each DLP there exists a uniform equivalent NLP.
Proof.Again,we give a step-by-step transformation.So,let be a disjunctive rule in a DLP,,and consider the program
with,
where is de?ned as in the proof of Theorem1.Note that the only difference between and is that here we just consider those triples from where.To proceed with the proof,observe that analogously to the proof of Theorem1,we get
(2)
We show.By Proposition4,this holds iff both
and hold.
We?rst show,which clearly implies imme-diately.Note that if is empty we are done,since then
holds trivially.So consider.We show that,for each and each,holds.Towards a contradiction,let ,,and suppose.On the one hand,since,we have(a),(b),and(c)for each SE-interpretation with,implies.On the other hand,satis?es the following conditions for being a counter SE-model of ,by Proposition7:(i),(ii),(iii),and(iv)or .We use(iv)for distinguishing between the following two cases: First,assume.Clearly,holds and by(i)and by(iii) hold.We get.Moreover,holds,since. By Lemma1,we get and holds by(a),i.e.,since. Hence,which clearly is in contradiction to(c).
Second,assume.By(iv),then.Together with(iii)we have
.Moreover,holds by(ii).Since,holds.
160Thomas Eiter et al.
Lemma1yields,and since,we have with .Again this is in contradiction to(c).
It remains to show.In fact we show with
.By inspecting(2),it is seen that implies
which shows the claim since
holds trivially.To derive,we show,for any
,that either or.So,?x some
.We consider two cases.
Assume.Hence,there exists a set such that .We know that.Thus,.We already have shown,yielding.But then, ,since.
So assume and thus.However,we have
,since none of the following conditions from Proposition7is satis?ed: (i),(ii),(iii),or(iv)and.For(i+ii)this is seen by the fact that and thus.(iii+iv)trivially fail.Hence,.
As already discussed above,the only program from our examples–which is not uniformly equivalent after replacing by is.However,since is closed under here-intersection,we already know how to derive a strongly(and thus uniformly) equivalent normal logic program from the proof of Theorem1.In fact,one can ver-ify that.For an example program which is not closed under here-intersection and has,with disjunctive,consider
over.The SE-models of are given as follows:
.
Indeed,is not closed under here-intersection.Let.We have that is given by and as can be veri?ed,.Moreover,
Only the last triple,,is applied in the construction of.In fact,we have to add(which is given by)to.For the resulting program,we then have,but the “critical”SE-interpretation,,has been eliminated.In fact,
holds,since neither nor is UE-model of.
5Ordinary Equivalence
Finally,we discuss how to derive normal logic programs which are ordinary equiva-lent to given disjunctive ones.By Theorem2,such programs always exist and,for a given program,clearly does the job,since uniform equivalence implies ordinary equivalence.However,we give two further alternatives.The?rst is motivated by an enumeration of stable models,while the second one optimizes.To start with,we state the following result which is easily seen from Proposition7.
Eliminating Disjunction from Propositional Logic Programs161
Proposition8.or,for any. Theorem3.Let be DLP.Then,with. Proof.Let.Then,for each,either or.By Proposition8,.Towards a contradiction,suppose.By
Proposition2,there exists a such that.In particular,we must have.But by Proposition8,it is easily seen that this is contradicted by .Thus,.
Conversely,suppose and.That is,
for some.Then,for each.We have, for each by Proposition8.Thus,with.But this contradicts.
The following construction would be more“structure-preserving”and,to some ex-tend,“optimizes”the program.
Theorem4.Let be DLP and.Then,with
with
Proof.Let.Obviously,and,by Proposition6,. Moreover,,which implies,by Theorem3,.Thus,.It remains to show that no,yields an SE-model of.Towards a contradiction, suppose some such that.Clearly,,hence, since,must hold.Then,by Proposition6,. We have and,and thus get by construction.By Proposition8,which contradicts .Thus,no with exists.This means.
Conversely,let.This implies.Towards a contradiction, suppose,i.e.,there exists,such that.By Proposition6,.Since,we have, for each.By Proposition8,for each with .Hence,.By Proposition2,this contradicts.
To summarize,given a DLP with disjunctive,we are able to construct(via a replacement of by normal rules)a logic program which is ordinary equivalent to ;a program which is uniformly equivalent to;and,whenever is closed under here-intersection,a program which is strongly equivalent to.All these programs are of the form
for
By de?nition of,we furthermore can state that and.Hence, our method can be seen as a uniform framework for all important notions of equiva-lence.Moreover,our results extend and generalize methods based on shifting disjunc-tions,since the outcome of these methods coincides with the presented rewriting, whenever is empty.In particular,concerning equivalence in terms of stable mod-els,we present a semantic criterion(in contrast to the syntactic criterion of head-cycle free programs,cf.[1])which allows for shifting.Concerning equivalence in terms of UE-models,we generalize an observation made in[7](see Theorem4.3).
162Thomas Eiter et al.
6Complexity Issues
Finally,we deal with some related complexity issues.We can express the test for a DLP of being closed under here-intersection via the following normal logic program, which is linear in the size of.
De?nition6.Let be a DLP over atoms and let,,,,,,and be disjoint new atoms.De?ne
(3)
(4)
(5)
(6)
(7)
(8)
(9)
Intuitively,the program works as follows.Rules(3)guess an interpretation of and rules(5)check that is a model of.Similarly,rules(4)guess subsets and of such that both are models of,which is enforced by(6).Hence,(3)–(6)’compute’all pairs of SE-models and of.
Now,rules(7)compute the intersection and via rules(8)the new atom can be derived iff the intersection does not model,i.e.iff is no SE-model of.The constraint(9)kills all models of for which this is not the case, i.e.for which is an SE-model of.Thus,(7)–(9)ensure that has no stable model iff is closed under here-intersection.Formally,we have:
Theorem5.A DLP is closed under here-intersection iff has no stable model.
Based on this,we derive the following complexity result.
Theorem6.Let be a DLP.Then,checking whether there exists a normal logic pro-gram strongly equivalent to is complete for coNP.
Proof.By Theorem5,and the linear encoding from De?nition6we get that closed-ness under here-intersection is in coNP.By Theorem1,we immediately get the coNP-membership part.
We show coNP-hardness of this problem by a reduction to the coNP-complete prob-lem of deciding whether is the unique model of a positive DLP.
Let be a positive DLP over the alphabet,let be new atoms,and consider the program
.
We prove that is closed under here-intersection iff is the unique model of.
The if direction is straight forward:If is the unique model of then,by con-struction,is the unique model of,and since is positive–and hence constant under reduction–is trivially closed under here-intersection.
Eliminating Disjunction from Propositional Logic Programs163 For the only-if direction assume is closed under here-intersection and,towards a proof by contradiction,suppose there exists a model of.Then both,
and are models of and thus also both,
and are SE-models of.However,is not an SE-model of,since.This contradicts the assumption that is closed under here-intersection,hence is the unique model of.
We have shown coNP-hardness of deciding whether a DLP is closed under here-intersection which immediately implies coNP-hardness of checking whether there ex-ists a normal logic program strongly equivalent to by Theorem1.
Another interesting issue is the size of the rewriting of a given DLP into an equivalent NLP(if it exists).Using the constructive methods presented in this paper the rewriting is of exponential size,in general.However there is strong evidence that this is unavoidable.Let and denote the classes of all DLPs and NLPs, respectively(over atoms).
Theorem7.For each-hard family of DLPs such that there exist-equivalent NLPs,there does not exist a polynomial rewriting such that, ,for every DLP of,unless the Polynomial Hierarchy(PH)collapses. Proof.(Sketch)Towards a contradiction,assume that for a positive DLP,a polyno-mial rewriting exists and consider the-hard problem of checking whether,for some atom,is a cautious consequence of([9]).
Then,we could guess an NLP in nondeterministic polynomial time. Furthermore,checking is in coNP(even in case of uniform equivalence,since is positive and is normal,i.e.head-cycle free[7]).As well,checking whether is in coNP(since is normal).Thus,the-hard problem of deciding
would be in,a contradiction unless PH collapses.
Also for rewritings under ordinary equivalence,we cannot avoid an exponential blow up unless PH collapses.
Theorem8.There is no polynomial rewriting such that
for every,unless PH collapses.
Proof.(Sketch)This can be shown by using nonuniform complexity classes as in[3,2, 13],following closely the line of proof there that the existence of a polynomial model-preserving mapping from propositional circumscription to classical propositional logic would imply that coNP poly,i.e.,the class of problems decidable in polynomial time with polynomial advice.This inclusion implies a collapse of PH.The proof can be easily adapted,where the mapping,,and
are replaced with,(positive),and,respectively.
Clearly Theorem7implies Theorem8,but the proof of the latter does not refer to non-uniform complexity classes,and is thus more accessible.We remark that in terms of[13],is a stronger formalism than unless PH collapses.Furthermore, Theorem8remains true for generalized rewritings which admit projective extra vari-ables,i.e.,,where is on atoms and denotes the restriction of the stable models of to the original atoms.Indeed,such an would imply coNP NP poly,which again means that PH collapses.
164Thomas Eiter et al.
7Conclusion
In this work,we derived new results on the relationship between propositional dis-junctive and normal logic programs under the stable model semantics,by investigating
whether disjunctions in a given program can be replaced by normal rules,in such a way that this modi?cation does not change the set of SE-models(resp.UE-models,
stable models)of.In a bigger picture,such a rewriting technique allows to obtain a strongly(resp.uniformly,ordinary)equivalent normal logic program from a given disjunctive logic program.
Our results show that under ordinary and uniform equivalence,this rewriting is always possible.In the case of strong equivalence we identi?ed an appealing semantic criterion based on so-called here-intersection.The rewriting itself is based on the well-known(local)shifting of disjunctive rules,but extends this method by an addition of further rules,which take the semantic of the entire program into account.Hence,this rewriting is in general hard to obtain,and has to be exponential in the worst case under widely accepted complexity theoretic assumptions.
These results complement recent considerations on simpli?cation techniques un-
der different notions of equivalence,cf.[22,30,8],and thus add to the foundations of improving implementations of Answer Set Solvers.
Moreover,we showed that the problem of deciding whether a DLP is closed under
here-intersection,i.e.,deciding whether there exists a strongly equivalent NLP,is com-plete for coNP,answering a question left open in[8].As a by-product,we presented an encoding of this test via a normal logic program.Note,however,that this test may also be treated by SAT-solvers.Thus,we also contributed to a line of research in ASP,which relies on the application of classical propositional logic(or QBFs)to deal with certain problems in logic programming[15,5,24].
Further issues concern a closer investigation of adding extra variables,as well as of the newly derived class of DLPs closed under here-intersection.One the one hand,we are interested in the expressibility of such programs.On the other hand,it is an open question whether this class allows for optimizations of algorithms used in disjunctive logic programming engines such as DLV.
References
1.R.Ben-Eliyahu and R.Dechter.Propositional semantics for disjunctive logic programs.
Annals of Mathematics&Arti?cial Intelligence,12:53–87,1994.
2.M.Cadoli,F.Donini,and M.Schaerf.Space ef?ciency of propositional knowledge repre-
sentation formalisms.Journal of Arti?cial Intelligence Research,13:1–31,2000.
3.M.Cadoli,F.Donini,M.Schaerf,and R.Silvestri.On compact representations of proposi-
tional circumscription.Theoretical Computer Science,182(1-2):183–202,2000.
4. D.J.de Jongh and L.Hendriks.Characterizations of strongly equivalent logic programs in
intermediate logics.Theory and Practice of Logic Programming,3(3):259–270,2003.
5.U.Egly,T.Eiter,H.Tompits,and S.Woltran.Solving advanced reasoning tasks using quan-
ti?ed Boolean formulas.In Proc.AAAI-00,pp.417–422.AAAI/MIT Press,2000.
6.T.Eiter,W.Faber,N.Leone,and G.Pfeifer.Declarative problem-solving using the DLV
system.In J.Minker,ed.,Logic-Based Arti?cial Intelligence,pp.79–103.Kluwer,2000.
Eliminating Disjunction from Propositional Logic Programs165 7.T.Eiter and M.Fink.Uniform equivalence of logic programs under the stable model seman-
tics.Tech.Rep.INFSYS RR-1843-03-08,Inst.f¨u r Informationssysteme,TU Wien,2003.
Preliminary Report.Short version in Proc.ICLP-03,to appear.
8.T.Eiter,M.Fink,H.Tompits,and S.Woltran.Simplifying logic programs under uniform
and strong equivalence.Manuscript,submitted,July2003.
9.T.Eiter and G.Gottlob.On the computational cost of disjunctive logic programming:Propo-
sitional case.Annals of Mathematics&Arti?cial Intelligence,15(3/4):289–323,1995. 10.T.Eiter and G.Gottlob.Expressiveness of stable model semantics for disjunctive logic
programs with functions.Journal of Logic Programming,33(2):167–178,1997.
11.T.Eiter,G.Gottlob,and H.Mannila.Disjunctive Datalog.ACM TODS,22(3):364-417,1997.
12.M.Gelfond and V.Lifschitz.Classical negation in logic programs and disjunctive databases.
New Generation Computing,9:365–385,1991.
13.G.Gogic,H.Kautz,C.H.Papadimitriou,and B.Selman.The comparative linguistics of
knowledge representation.In Proc.IJCAI-95,pp.862–869.Morgan Kaufmann,1995. 14.T.Janhunen,I.Niemel¨a,P.Simons,and J.-H.You.Partiality and disjunctions in stable model
semantics.In Proc.KR-00,pp.411–419.Morgan Kaufmann,2000.
15. C.Koch and N.Leone.Stable model checking made easy.In Proc.IJCAI-99,pp.70–75.
Morgan Kaufmann,1999.
16.V.Lifschitz,D.Pearce,and A.Valverde.Strongly equivalent logic programs.ACM Trans-
actions on Computational Logic,2(4):526–541,2001.
17. F.Lin.Reducing strong equivalence of logic programs to entailment in classical proposi-
tional logic.In Proc.KR-02,pp.170–176.Morgan Kaufmann,2002.
18.M.J.Maher.Equivalences of logic programs.In Minker[21],pp.627–658.
19.V.W.Marek,J.Treur,and M.Truszczy′n ski.Representation theory for default logic.Annals
of Mathematics&Arti?cial Intelligence,21(2–4):343–358,1997.
20.W.Marek and J.Remmel.On the expressibility of stable logic programming.Theory and
Practice of Logic Programming,3(4-5):551–567,2003.
21.J.Minker,editor.Foundations of Deductive Databases and Logic Programming.Morgan
Kaufman,Washington DC,1988.
22.M.Osorio,J.Navarro,and J.Arrazola.Equivalence in answer set programming.In Proc.
LOPSTR-01,LNCS2372,pp.57–75.Springer,2001.
23. D.Pearce.A new logical characterisation of stable models and answer sets.In Non-
Monotonic Extensions of Logic Programming(NMELP1996),LNCS1216,pp.57–70.
Springer,1997.
24. D.Pearce,H.Tompits,and S.Woltran.Encodings for equilibrium logic and logic programs
with nested expressions.In Proc.EPIA-01,LNCS2258,pp.306–320.Springer,2001. 25. D.Pearce and A.Valverde.Some types of equivalence for logic programs and equilibrium
logic.In Proc.Joint Conf.on Declarative Programming(APPIA-GULP-PRODE),2003. 26.T.Przymusinski.Stable semantics for disjunctive programs.New Generation Computing,
9:401–424,1991.
27.Y.Sagiv.Optimizing Datalog programs.In Minker[21],pp.659–698.
28.J.Schlipf.The expressive powers of logic programming semantics.Journal of Computer
and System Sciences,51(1):64–86,1995.Abstract in Proc.PODS90,pp.196–204.
29.H.Turner.Strong equivalence for logic programs and default theories(made easy).In Proc.
LPNMR-01,LNCS2173,pp.81–92.Springer,2001.
30.H.Turner.Strong equivalence made easy:nested expressions and weight constraints.Theory
and Practice of Logic Programming,3(4–5):609–622,2003.
控制软件说明书
控制软件说明书 PC端软件FTM 安装及应用 系统运行环境： 操作系统中英文Windows 98/2000/ NT/XP/WIN7/ Vista， 最低配置 CPU：奔腾133Mhz 内存：128MB 显示卡：标准VGA，256色显示模式以上 硬盘：典型安装 10M 串行通讯口：标准RS232通讯接口或其兼容型号。 其它设备：鼠标器 开始系统 系统运行前，确保下列连线正常： 1：运行本软件的计算机的RS232线已正确连接至控制器。 2：相关控制器的信号线，电源线已连接正确； 系统运行步骤： 1：打开控制器电源，控制电源指示灯将亮起。 绿色，代表处于开机运行状态；橙色代表待机状态。 2. 运行本软件 找到控制软件文件夹，点击FWM.exe运行。出现程序操作界面：
根据安装软件版本不同，上图示例中的界面及其内容可能会存在某些差别，可咨询我们的相关的售后服务人员。 上图中用红色字体标出操作界面的各部分的功能说明： 1. 菜单区：一些相关的菜单功能选择执行区。 2. 操作区：每一个方格单元代表对应的控制屏幕，可以通过鼠标或键盘的点选，拖拉的方式选择相应控制单元。 3.功能区：包含常用的功能按钮。 4.用户标题区：用户可根据本身要求，更改界面上的标题显示 5.用户图片区：用户可根据本身要求，更改界面上的图片显示，比如公司或工程相关LOGO图片。 6.附加功能区：根据版本不同有不同的附加项目。 7.状态区：显示通讯口状态，操作权限状态，和当前的本机时间，日期等。 如何开始使用 1. 通讯设置 单击主菜单中“系统配置”――》“通讯配置” 选择正确的通讯端口号，系统才能正常工作。 可以设置打开程序时自动打开串口。 2.系统配置
用造句子大全
路上的垫脚石，踏着它，走向成功。 12、初三让我受益匪浅，她让我明白了珍惜时间才不会虚度此 生的真谛，她让我懂得了珍爱人生就要去拼搏去奋斗的道理。如醉 如痴，她让我用**吮吸着知识的甘露；豁然开朗，她让我用真诚去 探寻着做人的美好。 13、普里尼曾说过：“在希望与失望的决斗中，如果你用勇气 与坚决的双手紧握着，胜利必属于希望。”的确啊，生活正需要这 种坚持不懈，永不放弃的精神。 14、十月国庆节，我又去外婆家，此时凤仙花的花瓣都凋落了，取而代之的是，枝上都挂满一个个鼓鼓的对象，爸爸汇报我那是凤 仙花的果子，内里有一粒粒的种子。我用手轻轻一捏，果子溘然 “爆炸”了，内里的种子像弹片一样。 15、大地啊，你是多么平反而有多么伟大，你用你的博爱征服 了无数的人们，让他们心甘情愿的像你一样无私奉献。 16、蚕宝宝还是天生的“歌唱家”，我用耳朵听蚕宝宝们吃桑 叶的时候，真的能听见“沙沙”的声音，那有节奏的沙沙声，像一 首百听不厌的乐曲。 17、我们学习的目的，是为了使用，不是知识没有用，而是你 没有使用，说明你没有用。 18、月光下，我用繁冗拖沓的文字祭奠我的青春，纪念我死去 的友情和迟到的爱情。 19、轻负担，高效率，教给学生有用的东西。 20、知识并非对人人都是同样有用的，正象权力不能使卑劣的 人变得高尚；知识也不能成为衡量人们心灵美丑的标准。 21、赏识不是单向的施舍，是智慧与智慧的主动碰撞；赏识不
是别有用心的廉价恭维，是对一种相对价值的公正认可；赏识不是 谀词满口的鄙俗奉承，而是对事物固有魅力的真诚。 22、人生好像火柴，严禁使用是愚蠢的，滥用则是危险的。 23、我用心与你握别，愿生活给你带来无数希望的翠绿，把你 引向理想的天地。 24、我爱学校的教室，因为教室让我获得了丰富的知识；我爱 学校的操场，因为操场让我拥有了健康的身体；我爱学校的老师， 因为老师让我成为了优秀的学生；我爱学校，因为学校把我培养成 了一个有用的人才！ 25、世界原本就不是属于你，因此你用不着抛弃，要抛弃的是 一切的执著。万物皆为我所用，但非我所属。 26、在不幸中，有用的朋友更为必要；在幸运中，高尚的朋友 更为必要。在不幸中，寻找朋友出于必需；在幸运中，寻找朋友出 于高尚。 27、金钱是一种有用的东西，但是，只有在你觉得知足的时候，它才会带给你快乐，否则的话，它除了给你烦恼。 28、不管作业有多少，都要按时完成，而且都要有质量的完成。切记，认真且有思考的完成一套卷，比走马观花的完成十套卷有用 的多。 29、童年中，岸上的那只老黄牛散漫的咀嚼夕阳，在村口母亲 的叫唤声中，蹒跚着步履将夕阳下的剪影拉长。时过境迁，梦境与 现实对视，我用一段韶光，苍老了一段年华。 30、低调做人，往往是赢取对手的资助、最后不断走向强盛、 伸展势力再反过来使对手屈服的一条有用的妙计。 31、不是学习没有用，而是因为我没用，因为我没用，所以我
linux 下各个头文件的作用
linux 下各个头文件的作用 2.6.30.4的头文件的位置和2.6.25.8的不一样，除去内核源码下的include目录外， 在arch/arm/mach-s3c2410/和arch/arm/plat-s3c24xx/目录下都有include目录的。 #include
智能窗户控制系统软件说明
智能窗户控制系统软件V1.0设计说明 目录 前言 (1) 第一章软件总体设计 (1) 1.1. 软件需求概括 (1) 1.2. 定义 (1) 1.3. 功能概述 (1) 1.4. 总体结构和模块接口设计 (2) 第二章控制系统的总体设计 (3) 2.1. 功能设计 (3) 第三章软件控制系统的设计与实现 (5) 3.1. RF解码过程程序设计介绍 (5) 3.2. RF对码过程设计 (6) 3.3. 通信程序设计 (8) 3.4. IIC程序设计介绍 (9) 3.5. 接近开关程序设计 (12) 3.6. 震动开关检测程序设计 (13) 3.7. 墙面按键程序设计 (15) 第四章智能窗户控制系统的设计 (17) 第五章实测与结果说明 (18) 第六章结论 (18)
前言 目的 编写详细设计说明书是软件开发过程必不可少的部分，其目的是为了使开发人员在完成概要设计说明书的基础上完成概要设计规定的各项模块的具体实现的设计工作。 第一章软件总体设计 1.1.软件需求概括 本软件采用传统的软件开发生命周期的方法，采用自顶向下，逐步细化，模块化编程的软件设计方法。 本软件主要有以下几方面的功能 (1)RF遥控解码 (2)键盘扫描 (3)通信 (4)安全检测 (5)电机驱动 1.2.定义 本项目定义为智能遥控窗户系统软件。它将实现人机互动的无缝对接，实现智能关窗，遥控开关窗户，防雨报警等功能。 1.3.功能概述 1.墙体面板按键控制窗户的开/关 2.RF遥控器控制窗户的开/关 3.具有限位，童锁等检测功能 4.实时检测大气中的温湿度，下雨关窗 5.具有防盗，防夹手等安全性能的检测
世界造句大全
世界造句大全 导读：本文是关于世界造句大全，如果觉得很不错，欢迎点评和分享！ 1、感谢对手，是他们让你成长；感谢母亲，是她给了你看到世界的机会；感谢父亲，是他握住你的手让你前进；感谢朋友，是他们在狂风骤雨的路上陪你一起走；感谢自然，是他教会了你一种感谢的心态。 2、雁荡山的美，是一种幽静的美。走进山林，人仿佛一下子被幽静包裹着，林中一丝声音也没有，仿佛是一个与外面截然不同的世界，一个与世隔绝的地方。直到一只突然醒悟的鸟儿长鸣一声，才打破了无声的世界。 3、爱的力量大到可以使人忘记一切，却又小到连一粒嫉妒的沙石也不能容纳当一个人真正觉悟的一刻，他放弃追寻外在世界的财富，而开始追寻他内心世界的真正。 4、如果不坚持，到哪里都是放弃。如果这一刻不坚持，不管再到哪里，身后总有一步可退，可退一步不会海阔天空，只是躲进自己的世界而已，而那个世界也只会越来越小。 5、春天，田野也披上了绿装，竹笋也从地下探出头来，呼吸着新鲜空气，看一看这奇妙的世界，柳树姑娘吐出了嫩芽，一阵微风吹来，它挥动着细长的胳膊跳起了婀娜多姿的舞美丽极了，令人陶醉。 6、他心里好像有种说不出的滋味，好像全世界的蛇胆都在自己
肚子中翻腾，他受不了，想把这种苦吐掉，但是这东西刚倒嘴边，又硬生生地咽了回去，空留他一口苦涩。 7、谢谢你，微风，是你用你那曼妙的身姿，舞动树梢，树叶飘零，"沙沙"直响，让我明白了原来的世界万物都有它的生命，它的语言。要用心灵去感受这个世界。 8、人生在世不容易，千万不要把烦恼当菜吃。你的快乐，就是真个的世界。小徒弟问我，师父啊你悟道了什么呢。我告诉他，很多年以后，不许空手来给我上坟，起码要带几个苹果。 9、世界最无私、最伟大、最崇高的爱，莫过于母爱。在我的学习生活中，妈妈给了我无微不至的关爱，在妈妈的关爱中，我健康、快乐地成长着。 10、花儿们竞相怒放，红的像火，白的像雪、粉的像霞，五光十色。山上的桃花远远望去像云霞。花儿们给世界穿了一件花衣裳，美丽极了。 11、黄昏，像我在佛前点燃的一柱香，心静时的苦苦惆怅，将一个个梦境，爱的心痛，继续燃放。一种感伤从心底抽出，拉长，直到光束无法触摸的地方。让黄昏触摸到自己内心深处的伤，这痛，隐藏在黑色的世界。 12、爱心是一柄撑起在雨夜的小伞，使漂泊异乡的人得到亲情的荫庇；爱心是一道飞架在天边的彩虹，使满目阴霾的人见到世界的美丽；爱心是一杯泼洒在头顶的冰水，使高热发昏的人得能冷静地思索；爱心是一块衔含在嘴里的奶糖，使久饮黄连的人尝到生活的甘甜。
软件操作说明书
门禁考勤管理软件 使 用 说 明 书
软件使用基本步骤
一．系统介绍―――――――――――――――――――――――――――――2二．软件的安装――――――――――――――――――――――――――――2 三．基本信息设置―――――――――――――――――――――――――――2 １）部门班组设置―――――――――――――――――――――――――3 ２）人员资料管理―――――――――――――――――――――――――3 ３）数据库维护――――――――――――――――――――――――――3 ４）用户管理―――――――――――――――――――――――――――3 四．门禁管理―――――――――――――――――――――――――――――4 １）通迅端口设置―――――――――――――――――――――――――4２）控制器管理――――――――――――――――――――――――――4３）控制器设置――――――――――――――――――――――――――6４）卡片资料管理―――――――――――――――――――――――――11 ５）卡片领用注册―――――――――――――――――――――――――12６）实时监控―――――――――――――――――――――――――――13 五．数据采集与事件查询――――――――――――――――――――――――13 六．考勤管理―――――――――――――――――――――――――――――14 1）班次信息设置――――――――――――――――――――――――――14 2）考勤参数设置――――――――――――――――――――――――――15 3）考勤排班――――――――――――――――――――――――――――15 4）节假日登记―――――――――――――――――――――――――――16 5）调休日期登记――――――――――――――――――――――――――16 6）请假/待料登记―――――――――――――――――――――――――17 7）原始数据修改――――――――――――――――――――――――――17 8）考勤数据处理分析――――――――――――――――――――――――17 9）考勤数据汇总―――――――—――――――――――――――――――18 10）考勤明细表—―――――――――――――――――――――――――18 11）考勤汇总表――――――――――――――――――――――――――18 12）日打卡查询――――――――――――――――――――――――――18 13）补卡记录查询—――――――――――――――――――――――――19
博思软件操作步骤
开票端操作说明 双击桌面“博思开票”图标，单击“确定”，进入开票界面： 一、开票： 日常业务——开票——选择票据类型——增加——核对票号无误后——单击“请核对票据号”——输入“缴款人或缴款单位”——选择”收费项目”、“收入标准”——单击“收费金额”。 （如需增加收费项目，可单击“增一行”） （如需加入备注栏（仅限于收款收据）），则在右侧“备注”栏内输入即可） 确认无误后，单击“打印”——“打印” 二、代收缴款书： 日常业务——代收缴款书——生成——生成缴款书——关闭——缴款——输入“专用票据号”——保存——缴款书左上角出现“已缴款”三个红字即可。 三、上报核销： 日常业务——上报核销——选择或输入核销日期的截止日期——刷新——核销。 （注意：“欠缴金额”处无论为正或为负均不可核销，解决方法见后“常见问题”）
常见问题 一、如何作废“代收缴款书” 日常业务——代收缴款书——缴款——删除“专用票据号”和“缴款日期”——保存——作废。 二、上报核销时出现欠缴金额，无法完成核销，或提示多缴。 1、首先检查有没有选择好截止日期，选择好后有没有点击“刷新”。 2、其次检查有没有做代收缴款书。注意：最后一张缴款书的日期不得晚于选择上报核 销日期。 3、若上述方法仍无效，则可能是由于以前作废过票据而未作废缴款书。解决方法： 首先作废若干张缴款书（直到不能作废为止），然后重新做一张新的缴款书。再核销。 三、打开“博思开票”时，出现“windows socket error：由于目标机器积极拒绝，无法连接。 （10061），on API’connect’” 单击“确定”，将最下面一行的连接类型“SOCKET”更换为“DCOM”，再点“连接” 即可。 四、如何设置密码 双击桌面“博思开票”，单击登录界面的右下方“改口令”输入用户编号、新密码和确认密码，单击“确认”即可。 五、更换开票人名称或增加开票人 进入开票系统——系统维护——权限管理 1、更换开票人名称：单击“用户编码”——删除“用户名”——输入新的开票人名称 ——单击“保存用户”即可。 2、增加开票人：单击“新增用户”——输入“用户编码”和“用户名”——单击“保 存用户”——单击新增的用户编码——将右边的“权限列表如下”下面的“所有”前的小方框勾上——单击右侧“保存用户权限”。 六、重装电脑系统 1、由于博思开票软件安装在D盘，所以重装电脑系统前无需做任何备份。 2、重装系统后，打开我的电脑—D盘，将“博思软件”文件夹复制到桌面上（或U盘）。 3、将安装时预留的安装光盘放入主机，打开后找到“票据核销及管理_开票端(江西欠 缴不能上报版)”（或者进入D盘----开票软件备份目录勿删文件夹里也可找到）。双 击，按提示点击“下一步”，直到“完成”。 4、双击桌面任务栏右下角“博思开票服务器”，将其关闭（或右键点击“博思开票服 务器”——“关闭服务器”）。 （这一步若找不到“博思开票服务器”，也可以用重启电脑来代替） 5、将刚才复制到桌面（或U盘）的“博思软件”再复制粘贴回D盘，若提示“此文 件夹已包含名为博思软件的文件夹”，点击下面的“全部”。 6、双击桌面“博思开票”——输入用户编码(001)——确定。 7、确认原来的票据数据没有丢失后，将桌面（或U盘）的“博思软件”文件夹删除。
三年级用再也造句大全
三年级用再也造句大全 导读：本文是关于三年级用再也造句大全，如果觉得很不错，欢迎点评和分享！ 1、叶子轻轻地摇动了几下，几颗小露珠就调皮地躲进了草丛，再也寻找不到它们了。 2、当你再也没有什么可以失去的时候，就是你开始得到的时候。 3、一个人泄露了秘密，哪怕一丝一毫，就再也得不到安宁了。 4、离开了学校，再也见不到亲爱的老师，再也见不到同学了。 5、他现在回到森林里来，想坐进他的箱子里去。不过箱子到哪儿去了呢？箱子被烧掉了。焰火的一颗火星落下来，点起了一把火。箱子已经化成灰烬了。他再也飞不起来了。也没有办法到他的新娘子那儿去。 6、缘分就是小时候最喜欢的那个玩具，一旦丢失了，也许再也找不回来。 7、小蛇不安的在我手掌中扭动，我想它也许根本就不需要我的怜惜，它怕被我温暖后再也无力游走。那样它就会失去自由。 8、除了能造福于人类的工作之外，世上再也没有什么事业能真正而永久的名声了。 9、我再也不会相信你了，再也不会为你买棒棒糖了！ 10、眼睛是心灵的窗户，假如我们失去了这宝贵的“心灵之窗”，那么在你的脑海将是一片黑暗，再也没有那美丽的颜色和那世间的欢
笑声，在别人嬉戏时自己却只能在旁边听着那欢笑声，那种感觉是多么孤独、多么无助啊！ 11、大家再也不要再为这件事发愁了，再也不用发牢骚了，老板已经答应我们的要求了。 12、在人的一生中，再也没有像青年时期那样强烈地渴望被理解的时期了。没有任何人会像青年那样沉陷于孤独之中，渴望被人接近与理解；没有任何人会像青年那样站在遥远的地方呼唤。 13、我们的眼泪打湿了我们的衣衫，我们手拉着手，看着太阳一点点落下去，看着旧光阴一点点落下去，我们晓得，许多多少东西，再也不会返来了。 14、凡属我离开他而独自体验的一切，再也不给我带来任何喜悦。我的一切德行只是为了使他高兴，然而，当我在他身边时，我感到自己的德行软弱无力。 15、夏天到了，雄北极熊再也不能到陆地上捕到食物了，不过好在北极熊天生就是游泳健将，而且身披一身御寒大衣，有时它们需要持续地游100公里去寻找食物。 16、如果你的思想再也溅不起浪花，这会比死亡更可怕。没有不可认识的东西，我们只能说还有尚未被认识的东西。 17、你失去了金钱，可以再挣；你失去了一生，便再也不能回头。 18、自那些茹毛饮血的祖先用笨拙的双手，把一块块兽肉烤出第一缕香烟时，火成了人类进步的动力，我们再也无法与之分开。
控制系统使用说明
控制系统使用说明 系统针对轴流风机而设计的控制系统, 系统分为上位监视及下位控制两部分 本操作为上位监控软件的使用说明: 1: 启动计算机: 按下计算机电源开关约2秒, 计算机启动指示灯点亮, 稍过大约20秒钟屏幕出现操作系统选择菜单, 通过键盘的“↑↓”键选择“windows NT 4.0”菜单，这时系统进入WINDOWS NT 4.0操作系统，进入系统的操作画面。 2：系统操作 系统共分：开机画面、停机画面、趋势画面、报警画面、主机流程画面、轴系监测画面、润滑油站画面、动力油站画面、运行工况画面、运行记录画面等十幅画面，下面就十幅画面的作用及操作进行说明 A、开机画面： 开机： 当风机开始运转前，需对各项条件进行检查，在本画面中主要对如下指标进行检查，红色为有效： 1、静叶关闭：静叶角度在14度
2、放空阀全开：放空阀指示为0% 3、润滑油压正常 4、润滑油温正常 5、动力油压正常 6、逆止阀全关 7、存储器复位：按下存储器复位按钮，即可复位，若复位不成 需查看停机画面。 8、试验开关复位：按下试验开关按钮即可，试验开关按钮在风 机启动后，将自动消失，同时试验开关也自动复位。 当以上条件达到时，按下“允许机组启动”按钮，这时机组允许启动指示变为红色，PLC机柜里的“1KA”继电器将导通。机组允许启动信号传到高压柜，等待电机启动。开始进行高压合闸操作，主电机运转，主电机运转稳定后，屏幕上主电机运行指示变红。这时静叶释放按钮变红，按下静叶释放按钮后，静叶从14度开到22度，静叶释放成功指示变红。 应继续观察风机已平稳运行后，按下自动操作按钮，启机过程结束。 B、停机画面： 停机是指极有可能对风机产生巨大危害的下列条件成立时，PLC 会让电机停止运转： 1、风机轴位移过大
心情造句子大全一年级
心情造句子大全一年级 1、每一天的心情从那里开始没关系，在哪里结束更重要。 2、人间最珍贵是友情；最浪漫的是爱情；最动人的是恋情；最想要的是真情；我最想见到的是你有好心情！祝你快乐。 3、她的心情仍然很好，口里滔滔不绝，满怀心花怒放。 4、在这值得高兴的日子里，唯有烟花，才能吐出我们那喜悦的心情；唯有烟花，才能烘托这喜庆的气氛。 5、生是一场旅行，在乎的不是目的地，是沿途的风景以及看风景的心情。 6、秋天，秋高气爽，让我们感觉到心情特别地舒畅。 7、弯月，反映这一份快乐心情，可怜九月初三夜，露似真珠月似弓；弯月，体现了一种世间长情，但愿人长久，千里共婵娟。 8、经过长久的努力，他终于获得国际肯定，悲喜交杂的心情一言难尽。 9、登上万里长城，眺望塞外风光，心情多么豪迈！ 10、朋友是午睡初醒的那杯清茶，用无限的甘甜滋润每一份快乐心情。 11、花儿在灿烂地微笑，鸟儿在快乐地欢叫，我的心情啊，像吃了蜜一样甜。 12、恍忽间明白：明媚的春天之所以如此的美，是因为它让人的心情在此刻绽放。 13、街边流浪狗的难受心情是只可意会，不可言传的。
14、他心如鹿撞，心砰砰的跳，心里七上八下，心情如激荡的湖水一样不平静。 15、幸福是什么？幸福是积极地生活态度，是一份好心情，是温暖的关爱，是真诚的赞美，是快乐的分享，是无私的奉献。 16、东方的第一缕曙光刺破黑暗，光明随着时间铺满天地，即使冷意昂然的冬天，万物也是用喜悦的心情来期待着温暖。 17、你不能左右天气，但你可以改变心情；你不能改变容颜，但你可以展现笑容；你不能样样顺利，但你可以事事尽力。 18、我看着这蔚蓝的大海，不由地哼起了歌，心情像迎着海风飞驰的帆船一样轻快。 19、你以什么样的心态去面对生活，你就会收获什么样的心情！ 20、今天是阴天，灰灰的天让人的心情也不舒服，大热天里竟破天荒感到冷。 21、阴天，总有种失落的感觉，心情也随之下沉。 22、你以为我是康师傅绿茶啊，天天都有好心情。 23、抬头仰望天空，美丽的云在空中飘动，会使我的心情像云一样轻松。 24、碧空，晴虹万里，阳光透过窗户，灿烂地折射在我的脸上。心情自然轻松愉快拉。 25、虽说自然阴晴无常，其实太阳永远高挂在天空；虽说心情亦会有悲有喜，但只要心中有阳光，微笑永远会展现在脸上。 26、玩具熊不管大风大雨，都会天天对着我笑，我不管有什么难
LINUX内核源文件介绍以及头文件介绍
LINUX 内核源文件介绍以及头文件介绍 LINUX 内核源文件介绍以及头文件介绍.txt两人之间的感情就像织毛衣，建立的时候一针一线，小心而漫长，拆除的时候只要轻轻一拉。。。。*******************LINUX 内核（0.11）源文件介绍****************** 1、内核源文件放置目录： | |————boot 系统引导汇编程序目录 | |————fs 文件系统目录 | |————include 头文件目录 | |————init 内核初始化程序目录 | |————kernel 内存进程调度、信号处理、系统调用等程序的目录 | |————lib 内核库函数目录 | |————mm 内存管理程序目录 | |————tools 生成内核Image文件的工具程序目录 | |————Makefile文件 | 2、引导启动程序目录boot 包含3个汇编语言文件，是内核源文件中最先被编译的程序。 功能：当计算机家电时引导内核启动，将内核代码加载到内存中，并完成系统初始化工作。 boot | |————bootsect.s 磁盘引导块程序，编译后会驻留在磁盘的第一个扇区中| |————setup.s 读取机器的硬件配置参数，并把内核模式system移动到适当的内存位置处 |
|————head.s 会被编译连接在system模块的最前部分，主要进行硬件设备的探测配置和内存管理页面的配置工作 | 3、文件系统目录fs 包含17个C语言程序 fs | |——buffer.c 管理高速缓冲区 | |——file_table.c 在0.11仅定义了一个文件句柄（描述符）结构数组 | |——ioctl.c 将引用kernel/chr_dev/tty.c中的函数，实现字符设备的IO 控制功能 | |——exec.c 主要包含一个执行程序函数do_execve() | |——fcntl.c 实现文件I/O控制的系统调用函数 | |——read_write.c 实现文件读/写和定位的三个系统调用函数 | |——stat.c 实现了两个获取文件状态的系统调用函数 | |——open.c 主要包含实现修改文件属性和创建与关闭文件的系统调用函数 | |——char_dev.c 主要包含字符设备读写函数rw_char() | |——pipe.c 包含管道读写函数和创建管道的系统调用函数 | |——file_dev.c 包含基于i节点和描述符结构的文件读写函数。 | |——namei.c 主要包括文件系统中目录名和文件名的操作函数和系统调用函数 | |——block_dev.c 包含块数据读和写函数 | |——inode.c 包含针对文件系统i节点操作的函数 | |——truncate.c 用于在删除文件时释放文件所占用的设备数据空间 | |——bitmap.c 用于处理文件系统中i节点和逻辑数据块的位图 |
威利普LEDESC控制系统操作说明书
LED-ECS编辑控制系统V5.2 用 户 手 册 目录 第一章概述 (3) 1.1LED-ECS编辑控制系统介绍 (3) 1.2运行环境 (3) 第二章安装卸载 (3) 2.1安装 (3) 2.2卸载 (5) 第三章软件介绍 (5) 3.1界面介绍 (5) 3.2操作流程介绍 (13) 3.3基本概念介绍 (21) 第四章其他功能 (25) 4.1区域对齐工具栏 (25) 4.2节目对象复制、粘贴 (26) 4.3亮度调整 (26) 第五章发送 (27) 5.1发送数据 (27) 第六章常见问题解决 (28) 6.1计算机和控制卡通讯不上 (28) 6.2显示屏区域反色或亮度不够 (29)
6.3显示屏出现拖尾现象，显示屏的后面出现闪烁不稳定 (29) 6.4注意事项 (31) 6.5显示屏花屏 (31) 6.6错列现象 (32) 6.7杂点现象 (32) 第一章概述 1.1LED-ECS编辑控制系统介绍 LED-ECS编辑控制系统，是一款专门用于LED图文控制卡的配套软件。其具有功能齐全，界面直观，操作简单、方便等优点。自发布以来，受到了广大用户的一致好评。 1.2运行环境 ?操作系统 中英文Windows/2000/NT/XP ?硬件配置 CPU:奔腾600MHz以上 内存:128M 第二章安装卸载 2.1LED-ECS编辑控制系统》软件安装很简单，操作如下：双击“LED-ECS编辑控制系统”安装程序，即可弹出安装界面，如图2-1开始安装。如图所示 图2-1 单击“下一步”进入选择安装路径界面，如图2-2，如果对此不了解使用默认安装路径即可 图2-2 图2-3 单击“完成”，完成安装过程。 2.2软件卸载如图2-2 《LED-ECS编辑控制系统V5.2》提供了自动卸载功能，使您可以方便的删除《LED-ECS编辑控制系统V5.2》的所有文件、程序组件和快捷方式。用户可以在“LED-ECS编辑控制系统V5.2”组中选择“卸载LED-ECS编辑控制系统V5.2”卸载程序。也可以在“控制面板”中选择“添加/删除程序”快速卸载。卸载程序界面如图2-4，此时选择自动选项即可卸载所有文件、程序组和快捷方式。 图2-4 第三章、软件介绍
财政票据 网络版 电子化系统开票端操作手册
财政票据(网络版)电子化系统 开票端 操 作 说 明 福建博思软件股份有限公司
目录 1.概述 业务流程 流程说明：
1.单位到财政部门申请电子票据，由财政把单位的基本信息设置好并审核完后，财政部门给用票单位发放票据，单位进行领票确认并入库。 2.在规定时间内，单位要把开据的发票带到财政核销，然后由财政进行审核。 系统登录 登入系统界面如图： 登录日期：自动读取主服务器的日期。 所属区划：选择单位所属区划编码。【00安徽省非税收入征收管理局】 所属单位：输入单位编码。 用户编码：登录单位的用户编码【002】 用户密码：默认单位密码为【123456】 验证码：当输入错误时，会自动换一张验证码图片； 记录用户编码：勾选系统自动把用户编码保存在本地，第二次登录不需要重新输入。 填写完正确信息，点【确定】即可登入系统。 进入系统 进入系统界面如图： 当单位端票据出现变动的时候，如财政或上级直管下发票据时，才会出现此界面:
出现此界面后点击最下方的确认按钮，入库完成。 当单位端票据无变动时，直接进入界面： 2.基本编码人员管理 功能说明：对单位开票人员维护，修改开票人名称。 密码管理 修改开票人员密码，重置等操作。 收发信息 查看财政部门相关通知等。
3.日常业务 电脑开票 功能说明：是用于开票据类型为电子化的票据。 在电脑开票操作界面，点击工具栏中的【增加】按钮，系统会弹出核对票号提示框，如图： 注意：必须核对放入打印机中的票据类型、号码是否和电脑中显示的一致，如果不一致打印出来的票据为无效票据，核对完后，输入缴款人或缴款单位和收费项目等信息，全部输入完后，点【增加】按钮进行保存当前票据信息或点【打印】按钮进行保存当前票据信息并把当前的票据信息打印出来；点电脑开票操作界面工具栏中的【退出】则不保存。 在票据类型下拉单框中选择所要开票的票据类型，再点【增加】进行开票。
三年级用果然造句大全
小学三年级造句例句 三年级上册造句例句三 一、常见关联词： 1.因为...所以...、2.不但...而且...、3.一...就...、4.不是...而是...、5.尽管...但 (6) 从不…也不…、7.如果…就…、8.只要…就…、 9.既…又…、10.即使…也…、11.无论…总是…、12无论…都…、13.不论…还…、 14.不仅…而且…、15.不但…还…、16.虽然…但是…、 17.不是…而是…、18、一会儿…一会儿、19、…是…20、有的…有的…还有的、 23、…像…一样… 二、例句 1.…因为…所以… 因为我们共同努力，所以竞赛取得胜利。 因为我考了一百分，所以妈妈带我去欢乐谷玩。 因为我们付出了努力，所以我们取得了成功。 2.不但…而且… 张叔叔不但书法写得好,下象棋更是一流. 王师傅不但会开车，而且会修车。 苹果不但很大，而且很甜。 小红不但聪明，而且能干。 3、一…就… 你一进来，我就知道你想要说什么了！ 他一紧张就结巴。 他一起床就去看书。 不是我偷了你的东西，而是小明嫁庄于我的。 不是凭你的实力就可以拿到奖学金，而是你爸爸用钱换来的。 不是一个人就可以战胜困难的，而是要我们大家团结协作才可以战胜困难。 5、尽管…但… 尽管这件事很难完成，但他还是做到了。 尽管我们尽了最大的努力，但这个方案还是失败了。 6、从不…也不… 我上学从不迟到，上课也不乱讲话。 他对待任何事都从不气馁，也不怀有侥幸心理。 7、如果…就… 如果我们共同努力，竞赛就能取得胜利。 如果我们齐心协力，就能把这件事情办好。 8、只要…就… 只要我们共同努力，竞赛就能取得胜利。 只要我一开口，他就会答应我的任何请求。 9、既…又… 劳动既是付出,又是回报,还能得到无限快乐! 阅读课外书既可增长知识与阅历，又能丰富我们的业余生活，还能从中体会他人的感受。 10、即使…也… 即使前面的路有多么艰险，也要向前冲。 即使你成功了，也不能骄傲。
linux下C编程详解
1)Linux程序设计入门--基础知识 Linux下C语言编程基础知识 前言: 这篇文章介绍在LINUX下进行C语言编程所需要的基础知识.在这篇文章当中,我们将会学到以下内容: 源程序编译 Makefile的编写 程序库的链接 程序的调试 头文件和系统求助 ---------------------------------------------------------------------------- ---- 1.源程序的编译 在Linux下面,如果要编译一个C语言源程序,我们要使用GNU的gcc编译器. 下面我们以一个实例来说明如何使用gcc编译器. 假设我们有下面一个非常简单的源程序(hello.c): int main(int argc,char **argv) { printf("Hello Linux "); } 要编译这个程序,我们只要在命令行下执行: gcc -o hello hello.c gcc 编译器就会为我们生成一个hello的可执行文件.执行./hello就可以看到程序的输出结果了.命令行中gcc表示我们是用gcc来编译我们的源程序,-o 选项表示我们要求编译器给我们输出的可执行文件名为hello 而hello.c是我们的源程序文件. gcc编译器有许多选项,一般来说我们只要知道其中的几个就够了. -o选项我们已经知道了,表示我们要求输出的可执行文件名. -c选项表示我们只要求编译器输出目标代码,而不必要输出可执行文件. -g选项表示我们要求编译器在编译的时候提供我们以后对程序进行调试的信息. 知道了这三个选项,我们就可以编译我们自己所写的简单的源程序了,如果你想要知道更多的选项,可以查看gcc的帮助文档,那里有着许多对其它选项的详细说明. 2.Makefile的编写 假设我们有下面这样的一个程序,源代码如下: /* main.c */ #include "mytool1.h" #include "mytool2.h" int main(int argc,char **argv) { mytool1_print("hello"); mytool2_print("hello"); } /* mytool1.h */ #ifndef _MYTOOL_1_H #define _MYTOOL_1_H
控制软件操作说明书
创维液晶拼接控制系统 软件操作指南 【LCD-CONTROLLER12】 请在使用本产品前仔细阅读该用户指导书
温馨提示:: 温馨提示 ◆为了您和设备的安全，请您在使用设备前务必仔细阅读产品说明书。 ◆如果在使用过程中遇到疑问,请首先阅读本说明书。 正文中有设备操作的详细描述,请按书中介绍规范操作。 如仍有疑问,请联系我们,我们尽快给您满意的答复。 ◆本说明书如有版本变动,恕不另行通知,敬请见谅！
一、功能特点 二、技术参数 三、控制系统连接示意图 四、基本操作 五、故障排除 六、安全注意事项
一、功能特点创维创维--液晶液晶拼接拼接拼接控制器特点控制器特点 ★采用创维第四代V12数字阵列高速图像处理技术 视频带宽高达500MHZ，应用先进的数字高速图像处理算实时分割放大输入图像信号，在多倍分割放大处理的单屏画面上，彻底解决模/数之间转换带来的锯齿及马赛克现象，拼接画面清晰流畅，色彩鲜艳逼真。 ★具有开窗具有开窗、、漫游漫游、、叠加等功能 以屏为单元单位的前提下，真正实现图像的跨屏、开窗、画中画、缩放、叠加、漫游等个性化功能。 ★采用基于LVDS 差分传送技术差分传送技术，，增强抗干扰能力 采用并行高速总线连接技术，上位控制端发出命令后，系统能快速切换信号到命令指定的通道，实现快速响应。 采用基于LVDS 差分传送技术，提高系统抗干扰能力，外部干扰对信号的影响降到了最低，并且，抗干扰能力随频率提高而提升。★最新高速数字阵列矩阵通道切换技术 输入信号小于64路时，用户不需要再另外增加矩阵，便可以实现通道之间的任意换及显示。 ★断电前状态记忆功能 通过控制软件的提前设置，能在现场断电的情况下，重启系统后，能自动记忆设备关机前的工作模式状态。 ★全面支持全高清信号 处理器采用先进的去隔行和运动补偿算法，使得隔行信号在大屏幕拼接墙上显示更加清晰细腻，最大限度的消除了大屏幕显示的锯齿现象，图像实现了完全真正高清实时处理。纯硬件架构的视频处理模块设计，使得高清视频和高分辨率计算机信号能得到实时采样，确保了高清信号的最高视频质量，使客户看到的是高质量的完美画质。
工会经费收入专用收据(1)
工会经费收入专用收据(1) 福州博思软件开发有限公司 2010年6月 目录 第一部分初始安 装 ....................................................... (1) 1.1系统 安装 (1) 1.2系统登录 ............................................................ (4) 第二部分组成模块介 绍 ................................................... (4) 2.1模块组 成 (4) 2.1.1票据资料 .......................................................... (5) 2.1.2用户管 理 .......................................................... (5) 2.1.3 票据领用 (6) 2.1.4电脑开票 .......................................................... (6) 2.1.5手工开 票 .......................................................... (7) 2.1.6 手工批开票 (7) 2.1.7票据查询 .......................................................... (8) 第三部分软件操 作 ....................................................... (9) 3.2用户 管理 (10)
用终于造句子大全
用终于造句子大全 导读：本文是关于用终于造句子大全，如果觉得很不错，欢迎点评和分享！ 1、雨不停地下着，震耳欲聋的雷声还在轰鸣着。终于，天亮了，雨也渐渐小了，开始像布一样，接着又像帘子，像断了线的珠子，像一根根线，最后只能看地上的雨点来辨认雨的大小了。 2、也许一个人最好的样子就是静一点，哪怕一个人生活，穿越一个又一个城市，走过一条又一条街道，仰望一片又一片天空，见证一场又一场离别，于是终于可以坦然的说，我终于不那么执着。 3、因为我的寒窗苦读，不断积累知识，我的成绩终于提高了。 4、我的初中生活，也应该起源于我与重点学校的际遇，在不懈的努力下，我终于迎来了这段奇妙的，来之不易的，与华辰学校的尘缘。这美好的三年将为我展开不同寻常的体验。 5、火红的太阳终于挣开白云的纠缠，露出半个笑脸。天空中几小朵白云，像镶了金边的茉莉花，从云缝中冲出来。晨纱渐渐地碎了，缭绕着，盘旋着，像一缕缕轻烟袅袅升起，把金色的阳光洒在山坡上，照在勤劳的人们的笑脸上。 6、太阳把天空染得通红，大地也涂上一片鲜红的油彩。缓缓地，太阳终于升到了高空，顿时，太阳金灿灿的，浑身闪着刺眼的光芒，犹如一个大火球。 7、晚霞映红了整个西边天空，仙人球关闭的花蕾终于开放了，
先是花蕾中间鼓了起来，最后花尖也绽开了，越来越大，终于完全舒展开来。 8、有一个人，教会你怎样去爱了，但是，他却不爱你了。以后，我再也不会奋不顾身的去爱一个人了，哪怕是你。我终于明白，人这一辈子，真爱只有一回，而后即便再有如何缠绵的爱情，终究不会再伤筋动骨。 9、经过昨天的语文检测，我终于拿到了第一名。 10、小草的道路是曲折的，前途是光明的。它仅凭着薄瘠的黄土，与命运搏斗，同顽石争雄，经过顽强的奋斗，终于带着希望，露面于光明世界。 11、丝丝缕缕的光线透过树缝，地面上有无数光斑在摇曳，周围绿意盎然。晶莹的汗珠在青丝间悄然滑落，沉重的脚步终于迈过了最后一级石阶，“南天门”三个大字在眼前印刻，已经偏过几十度角的太阳微笑地望着胜利的我。 12、太阳拖着沉重的步伐，慢慢儿，一步一步地，努力向上面爬起来。到了最后他终于爬上了云霞，完全爬出了海面。 13、我不知道我现在做的哪些是对的，那些是错的，而当我终于老死的时候我才知道这些。所以我现在所能做的就是尽力做好每一件事，然后等待着老死。心中装满着自己的看法与想法的人，永远听不见别人的心声。 14、太阳终于羞答答的移了上来，一小步再一小步。 15、真正影响着我的并不是他的言语，而是他的人格魅力，他
linux下socket编程常用头文件
linux下socket编程常用头文件 sys/types.h：数据类型定义 sys/socket.h：提供socket函数及数据结构 netinet/in.h：定义数据结构sockaddr_in arpa/inet.h：提供IP地址转换函数 netdb.h：提供设置及获取域名的函数 sys/ioctl.h：提供对I/O控制的函数 sys/poll.h：提供socket等待测试机制的函数 其他在网络程序中常见的头文件 unistd.h：提供通用的文件、目录、程序及进程操作的函数 errno.h：提供错误号errno的定义，用于错误处理 fcntl.h：提供对文件控制的函数 time.h：提供有关时间的函数 crypt.h：提供使用DES加密算法的加密函数 pwd.h：提供对/etc/passwd文件访问的函数 shadow.h：提供对/etc/shadow文件访问的函数 pthread.h：提供多线程操作的函数 signal.h：提供对信号操作的函数 sys/wait.h、sys/ipc.h、sys/shm.h：提供进程等待、进程间通讯（IPC）及共享内存的函数 建议：在编写网络程序时，可以直接使用下面这段头文件代码 #include