text:
A Semantical Perspective on Verification of Knowledge
- Bernice Green
- 2 years ago
- Views:
1 A Semantical Perspective on Verification of Knowledge Paul Leemans, Jan Treur, Mark Willems Vrije Universiteit Amsterdam, Department of Artificial Intelligence De Boelelaan 1081a, 1081 HV Amsterdam The Netherlands URL: Abstract The usual approaches to verification of knowledge in the literature have a rather practical nature, and are sometimes ad hoc and depending on the syntactical structure of a particular knowledge representation language in the definitions of the properties that are tested. In this paper a more principled investigation provides a well-defined semantical basis, independent of any particular syntactical representation, of the various properties that can be tested, and their logical relationships. Central in this unifying semantical framework is the notion of domain description and the forcing relation that is used as a standard for the inferences. Properties covered include consistency, three variants of soundness, three variants of completeness, empirically foundedness, and wellinformedness. Keywords: Verification, knowledge, semantics, consistency, soundness, completeness, empirical foundation, well-informedness. 1 Introduction With the widespread use of knowledge in some form of representation, the need for verification of knowledge has become more important. In situations where knowledge-based systems support or even replace people, reliability and correct performance are of major importance; e.g., [20], [37]. An automatic verifier can serve as a very useful tool during the development of a (knowledge-based) system. It makes it possible to check the knowledge, prior to testing by identifying, for example, inconsistency, incorrectness, redundancy, and missing knowledge, thus supporting the knowledge engineer in the knowledge elicitation and modelling process; e.g., [29]. 1.1 Syntactic versus Semantic Perspective on Verification Knowledge and domain specific information are commonly described by specific representation languages, such as rules, decision tables, frames or objects. In most literature on verification and validation (V&V) of knowledge systems a rule-based representation language is considered. The reason for this is that they are the most often practically used representation of knowledge implemented. A number of existing approaches to knowledge base verification can be found in [1], [5], [9], [14], [15], [16], [17], [18], [19], [21], [22], [23], [24], [25], [26], [28], [29], [30], [31], [32]; in [37] a comparative overview can be found for some of the existing approaches. As argued in [37], one of the problems in almost all of the existing approaches to knowledge base verification is that both the properties addressed (e.g., consistency, correctness, completeness) and the techniques used for verification strongly depend on the knowledge 1
2 representation language in which the knowledge base is expressed. Most references address the case of rule-based knowledge representation; e.g., [22], [23], [24], [26], [30], [31], [32]. Other contributions focus on decision tables (e.g., [5]), frames (e.g., [6]), or other representation languages. This dependency on a specific knowledge representation language leads to ad hoc syntactical definitions of the properties, to problems in the transfer of the approaches from one knowledge representation formalism to another one, or problems in combing them in hybrid knowledge bases, e.g., knowledge bases combining rules and objects with inheritance (cf. [37]). Most of the anomalies are checked, in practice, for the case of rule-based knowledge representation by considering the syntactic form of the rules: syntactic verification. Such properties are not directly interpretable independent of the knowledge representation format used: they are not semantic notions. The main aim of this paper is to propose semantic notions, and to relate syntactic notions from the literature to these semantic notions. In [37] one of the research issues identified as to be addressed in more depth is theoretical foundations, in the sense of formal semantics for knowledge base anomalies. This paper indeed contributes such semantical foundations of a major part of the notions known from the literature on verification of knowledge. Moreover, to define the semantics of these various notions, one unifying semantical framework is offered. 1.2 The Role of Situation-Specific Information Reasoning processes as performed by human expert consultants or knowledge-based reasoning systems often involve an interaction with the outside world (e.g., a user or sensor) to obtain the situation-specific information needed in the reasoning. Therefore two collaborating roles for providing knowledge may be distinguished: the role of the reasoner (or reasoning system) is to provide (domain-specific but) situation-independent domain knowledge, while the role of the client or user is to provide situation-specific domain knowledge (information). The interactive reasoning, which results from this collaboration, combines these two types of knowledge. From the viewpoint of the reasoner, the knowledge acquired from the client or user may be viewed as domain information "from outside", in contrast to the reasoner s own (internal) domain knowledge. In [38], which inspired our view on interactive reasoning, the situation-specific information is represented by a so-called simulation structure, in contrast to the knowledge base, which is represented as a logical theory. From the logical perspective a simulation structure is a model of the theory defined by the knowledge base. To obtain adequate criteria for such an interactive reasoning process to draw correct conclusions, suitable definitions are needed of notions of soundness and completeness with respect to the given domain. Basically verification can be described as a comparison between 2
3 the behaviour of a knowledge base (KB) and the requirements. But for more complex knowledge bases it is not so clear how one should state these requirements. One could imagine the expert to specify the input-output correspondence of the component by means of a table defining the functionality. This is similar to the approach in [9] where a table of atoms is given that specifies what cause leads to which effects. In this paper we will introduce a particular view of verification by considering these requirements essentially as a domain description defining the possible situations (W), and determine the standards for derivation from it. Theoretically this domain description should be seen as the set of all possible situations that can occur (e.g., at different times). Obviously, listing this is not possible in a practical setting especially if the number of possible situations is very large. A useful idea for verification, in this case, is either to consider a smaller set of typical (crucial) situations, which can be used as a test-set, or define the set of world situations by a set of constraints. We will introduce a number of properties that can be attributed to a KB in relation to W, and are interesting for verification. We will show that the usual approach to verification is to check for special (usually syntactically defined) cases of these more general semantic notions. Verification, in our view, is essentially a comparison between the domain description W and the knowledge base KB. 1.3 The Potential Problems Errors in a knowledge base can arise through a variety of reasons. The simplest source of errors is, of course, the typographical mistake. An other, often occurring source of error is the alteration of the system knowledge in order to accommodate wider application coverage. Adding, changing and refining knowledge base elements can easily lead to problems. Yet another source of error is ignorance or limited knowledge of the expert or the knowledge engineer, which can very well lead to a system with incorrect or non-specific recommendations. The larger the knowledge base, the more difficult it is to see whether there are errors in the knowledge base. Knowledge base properties addressed in this paper are in the first place: Consistency properties No conflicting conclusions can be made from valid information (see Section 3), Soundness properties No invalid inferences can be made from valid information. In Section 3 three variants of definitions of soundness are put forward, which, however, (as shown in Section 3), if the inference relation is monotonic, semantically are equivalent. Completeness properties No deficiency: no valid information fails to produce desired conclusions. A more indepth analysis reveals that at least three semantically different variants of completeness can be identified (Sections 4 to 6). 3
4 A Prolog programme, DES-CHECK has been developed to check a knowledge base on these notions. In addition to these properties some other useful and related properties are identified such as implicit definability, explicit definability, and empirically foundedness of a domain (Section 5), and well-informedness of a knowledge base (Section 6). Moreover, a number of theorems established the logical connections between the notions. In Section 7 it is shown how the perspective put forward here can be used to verify more complex knowledge-based systems. It is addressed what kinds of properties are needed in example compositional model: a generic process model for diagnosis. In Section 2 the basic concepts needed for the rest of the paper are presented. The paper concludes with a discussion in Section 8. 2 Basic Semantic Concepts Knowledge bases and situation-specific information are commonly described by representation languages, such as rules, decision tables, frames, or objects. However, qua representation the expressive power of a large class of languages essentially does not exceed that of propositional logic, especially taking into account that within representations variables often (like in logic programming) can be eliminated by replacing them by all possible instances that are relevant in a certain context. Of course for the computational aspects of inferencing it may make a lot of difference whether and how variables or other abstractions are used; however, these inference process aspects are not addressed here. For a discussion on how object-, frame like or object-attribute-value representations as often used in knowledge system development environments can be related to the semantical propositional formalisation used in this paper, see Section 2.2, between Definition 2.2 and 2.3. Therefore, as we are interested in semantical properties of a system, rather than computational or visual properties, a propositional approach suffices here: we will focus on the sets of (ground) atoms that can be built in a given language rather then on the language itself. In this manner we can abstract from the specific language that is dealt with. Logical means are used to define two types of entities for a system, the knowledge and the facts. In logic it is not common to distinguish input facts versus output facts. Also a set of possible situations is hardly ever considered explicitly (rather the model theoretic semantics of a knowledge base defines such a set implicitly). We will show that both these distinctions are important for dedicated foundations of verification. As discussed above our approach exploits a description of the world. Such a description is given by a set of situation models, each describing a possible or typical situation of the world. The whole set describes either the set of all possible situations or a set of typical test cases. In short, verification should check whether the output that is derived from an input is desirable with respect to this world. 4
5 2.1 Situation Models In our language situations are described by a finite signature Ï, a sequence of (ground) atoms based on any given language. In a reasoning component one can distinguish three kinds of atoms according to the three subsets of the set of ground atoms At(Ïbased on Ï. At(Ï = InAt(Ï) InternalAt(Ï) OutAt(Ï) They are called the input atoms, the private or internal atoms, and the output atoms. One should note here that in the literature this is a less common distinction as usually it is assumed that any atom of a signature can be given (input) or queried (output). However, in accordance with software engineering principles on information hiding, in practice this is a very useful distinction. The sets of input and output atoms are disjoint from the set of internal atoms, but they are not necessarily disjoint from each other. Here, the input atoms describe facts that are influenced or observed from outside the system, the output atoms are those that one is interested in, and the internal or private atoms are those that can be used to determine the relation between input and output. The latter function as a sub goal or intermediate step in the derivations. In an inference they are derived from inputs (or other intermediary atoms) and are then used to continue the inference so as to reach the outputs (i.e. they subsequently serve as conditions in other rules). A useful notation is an ordered tuple Ï = < s 1, s 2,. ; i 1, i 2,. ; h 1, h 2, > that groups together the input, internal, and output atoms, respectively. Obviously, the s s, the i s and the h s can be arbitrary words, like flu, defect(cd_dirty) and temperature(dog, high). The propositional equivalent of an atom with a variable is the set of all instantiations of the variables; for instance defect(x: OBSERVATIONS) is equivalent to the set of atoms defect(cd_dirty), defect(cd_upside_down), etc. where X is instantiated by all objects that have been declared for the sort OBSERVATIONS. Definition 2.1 An actual situation is described as a (complete) situation model (or complete model) N that is a truth-assignment to the atoms in a signature Ï, i.e., a mapping N : At(Ï) µ {0, 1}. The set of complete models for signature Ï is denoted by CMod(Ï). The concise way to show the truth assignments is to give an ordered tuple of truth-values 0 or 1 that is in agreement with the signature Ï(e.g., see the example world description below). A domain (or world) description is a set W of situation models, i.e., any subset W CMod(Ï). 5
6 As an example consider the following world description W = { N 1, N 2, N 3 } with respect to the signature Ï = < s 1, s 2, s 3, s 4, s 5 ; i 1 ; h 1, h 2 > where N 1 = < 1, 0, 1, 0, 0 ; 1 ; 1, 0 > N 2 = < 1, 0, 0, 1, 0 ; 1 ; 0, 1 > N 3 = < 0, 1, 0, 0, 1 ; 0 ; 1, 0 > In principle the world could be described extensionally, by listing explicitly all possible (or interesting) situations. If the set of ground atoms is finite, as often is the case in practice, the set of all possible world situations will be finite. During knowledge engineering this set can often only be acquired in the form of a sample of (the most characteristic) situation models. Another way to describe these situations is to give a set of axioms that serve as constraints for the situations, see also [14], [15]. In this case a world description is the set of all possible situations that fulfil these constraints, which often can be chosen in such a way that a finite set remains (e.g., by giving bounds to numerical variables). However, when one wants to define foundations of verification, one can abstract from this issue and just assume that a set of situations is defined, leaving open the manner in which this set of situations is described. In this paper, sometimes the set is assumed finite, but then this will explicitly be stated. In order to express facts about the domain more conveniently it is possible to build up propositions from the atoms in our signature using the logical signs ª(conjunction: and), Ó(disjunction: or), (implication: if... then...) and Å (negation: not). When an arbitrary proposition p is true / holds in some situation model N we will use the truth relation symbol to write N p. A literal is a proposition that is either an atom or a negation of an atom, and for an arbitrary signature Ï we distinguish the sets of input literals (sometimes also called observables) InLit(Ï), and the set of output literals (sometimes also called hypotheses) OutLit(Ï). Furthermore ~c is defined as ÅEif c is an atom and as a if c = a. 2.2 Information States and Knowledge Bases It is appropriate to distinguish the models that reflect situation specific information of a domain from the knowledge base, KB, that gives the general information about a domain. The goal of such a knowledge base is to establish a relationship between the input and output facts of a signature, so when given some input facts the knowledge base should be able to derive some output facts. In general a system does not have full access to the actual situations. Indeed, it is the (unobservable) output part of these situations that one is interested in. Moreover, at a certain moment in time only some of the observations may be available, and only some of the 6
7 conclusions that may be drawn have been derived. For example, when a reasoning component starts to reason, not all input facts of a situation need to be known at that moment, and no conclusions have been derived yet. Therefore the following is defined (cf. 13]): Definition 2.2 A partial model M is a mapping M : At(Ï) µ {0, 1, u} For a many-sorted predicate logic variant, see [12]. Such a partial model describes the (current) information state of the reasoning component. We will sometimes omit the word partial and simply use the word model for a partial model. A partial model that has no unknown atoms (a situation model, for instance) is a complete model. In an implementation of a knowledge base in an Knowledge System Development Environment, the information state of the component is represented by what is often called the (dynamic) facts base. The facts in the facts base are usually represented by objects and attributes of them. We will show how such representations can be formalized in the form of a partial model. An attribute with a Boolean value such as in bird1.female = false encodes the information that the atomic statement female(bird1) is false; this corresponds to the symbol 0 in a partial model, assigned to the atom female(bird1). Similarly, a Boolean value true corresponds to a symbol 1 in a partial model; for instance male(bird1) has the truth value 1. An attribute with a non-boolean value codes a set of atomic statements. For example the expression bird1.color = grey stating that the attribute colour of bird1 has the value grey, encodes the information that the propositional atomic statement colour(bird1, grey) is true. In the same time we can have the information that colour(bird1, red) is false. The attributes for which no values are filled in in the objects base may be interpreted as unknown or as undefined. These express the partiality of the information state; they correspond to the symbols u in a partial model. Assume that we do not have information about the attribute size. Then both size(bird1, tall) size(bird1, small) are unknown. So this for simple example we can build the partial model, corresponding to <female(bird1), male(bird1), colour(bird1, grey), colour(bird1, red), size(bird1, tall), size(bird1, small)> in the following manner: 7
8 < 0, 1, 1, 0, u, u > Notice that there may be some dependencies between the different atoms. We will not discuss these at this place. Definition 2.3 Associated with any (partial) model M we define the input model In(M) that copies the input truth-assignment of M, but assigns u to all other atoms, and similarly the output model Out(M). In connection to a world description W we define the sets In(W) and Out(W) as the sets of input models respectively output models that are associated to the situations in W. Å ª\ 1 0 u Ó\ 1 0 u µ\ 1 0 u u u u u u u u 0 u u 1 u u u 1 u u Figure 1 Strong Kleene truth tables Because we use Strong Kleene semantics (cf. [13]; see Fig. 3), the truth or satisfaction relation applies to partial models too, and we can express the truth of a proposition p in a (partial) model M by M p. This naturally leads to an alternative representation of partial models by a set of literals, i.e. the set of all literals that are true in M. Thus all atoms mentioned in this set are known (either true or false), whereas the literals not in the set are assumed to be unknown. Yet another way to represent such a partial model is by a proposition: the conjunction of the literals in the related set of literals. This conjunction will contain all literals that are known, and any atom that does not occur has truth-value unknown. Note that we are using partial logic here. This has a relation to the fact that we do not assume the closed world assumption, so negations must be explicitly observed, or deduced. An essential part of partial logic is the refinement relation as defined below: This can be understood by defining a partial ordering on the set of truth values by u < 0, and u < 1. Definition 2.4 Let M and N be two arbitrary partial situation models with respect to a signature Ë. Now N is a refinement of M, denoted by M N, if for all atoms a #VËit holds /C 0CEquivalently, M N ²jc.KVËM c N c 8
9 Derivation or inference in our view is a process that sequentially derives new facts from old ones, thus always refining the partial model representing the current information state. In essence, we view inference as a process of refinement, and in particular we would like to refine the (observable) input model to the complete model that describes the actual situation that is under consideration. Here the following property is essential. Lemma 2.5 For any (partial) model M, it holds In(M) M. Another important property of input models is that they maintain the refinement ordering. Lemma 2.6 For any two (partial) models M, N UWEJVJCVM N it holds: In(M) In(N) Given a set of models V it is sometimes useful to consider the set P(V) of partial models that can be refined to a model in V. For a world description W the set P(W) can be viewed as the search space of the system. Reasoning is a process that starts with a partial situation model or information state, and subsequently tries to refine this model until an answer is found. The set P(In(W)) gives us the set of all possible (partial) inputs of a domain. As we stated before in the literature the set of possible inputs is often described by a set of constraints that an input model must obey. The following lemma is useful when using the operator P. Lemma 2.7 For any world description W, we have P(In(W)) = In(P(W)). We base our notions on a given inference relation that is assumed monotonic and sound but not necessarily complete (for example chaining, or unit resolution, or Horn resolution, or full resolution). Based on this given (generic) inference relation any language that is used to formulate a knowledge base will have an associated (specific) inference relation; the notation M KB p denotes that a proposition p can be inferred from the information represented in a model M by the inference relation associated with KB. In fact we consider as a ternary relation (instead of a binary relation as usual) due to our strict separation of situation independent domain knowledge from situation-specific information. For a knowledge base in rule format (if-then-rules) an obvious inference relation is chaining. Our rule format will consist of implications that have only one literal as conclusion, and a conjunction of literals as their condition. Having a negation in a conclusion is sometimes not allowed in the literature (if one restricts oneself to Horn-clauses, for instance). Continuing the example above we shall consider the following KB for the signature 9
10 Ï= < s 1, s 2, s 3, s 4, s 5 ; i 1 ; h 1, h 2 >. s 1 ª Å s 2 µ i 1 Å s 5 µ Å i 1 i 1 ª s 3 µ h 1 i 1 ª s 4 µ h 2 We will list some criteria that are useful to enforce on an inference relation. Conservativity seems obvious, that what is already known in a model can be derived from it (and, in fact cannot be overwritten by other inferences). Monotonicity implies that a larger input should infer a larger output. Chaining is an example of an inference relation that obeys these properties. Definition 2.8 Given a knowledge base KB, any proposition p, and arbitrary models M, N P(W), all with respect to a signature Ë, we distinguish the following properties for the inference relation related to the knowledge base: - conservativity M p implies M KB p. - monotonicity In(M),Q1 implies In(M) KB p In(N) KB p. Even though monotonicity seems very intuitive, in practice it is not used in many systems. A frame system, for instance, may specify default attribute values. These defaults are assumptions that may be (non-monotonically) retracted later. Also systems that use the Horn clause subset of predicate logic are often non-monotonic. They often apply the closed world assumption and the absence of an atom is interpreted as a negation. This negation may need to be retracted when the atom later becomes known. In this paper monotonicity is important for verification of properties like correctness, and soundness. 2.3 Forcing A question one might ask oneself in light of verification is how one should specify the desired behaviour of a reasoning component. One could imagine the expert to specify the inputoutput correspondence of the component by means of a table defining the functionality. This is similar to the approach in [9] where a table of atoms is given that specifies what cause leads to which effects. Our idea is to just consider the domain description W itself, and try to determine the standards for derivation from it. Here we consider the fact that some relation specifies what a knowledge base should derive. 10
11 Definition 2.9 Given a domain description W with respect to a signature Ï, a partial model M 29, and an output literal h OutLit(Ï). The model M forces the literal h within W if and only if h holds in every complete refinement N W with N M. We will use the notation that is defined by: M h ²jN W [ N M 0 h ] In a way this notion sets a standard for the knowledge base, what are the hypotheses it should derive given some partial model. Before we proceed we will mention a number of useful properties of forcing. Lemma 2.10 a) For any model M P(W) and proposition p it holds M p M p b) For any two models M 1, M 2 P(W) and proposition p such that M 1 M 2 it holds M 1 p M 2 p Here a) is trivial; the proof of b) runs as follows. If N M 2 VJGP N 0 1 which together with M 1 h implies N Jfor arbitrary N W. We have M 2 h. In general the properties for forcing and inference are closely related, and what is natural for forcing can be enforced on inference. The main theme of this paper is that this is what verification should check. The following corollary parallels conservatism and monotonicity, if one remembers Lemma 2.6 by which M N implies In(M) In(N). Like monotonicity does for inference, the following corollary then says for forcing that a larger input model forces a larger output. In fact this may be seen as the reason for assuming monotonicity of inference in the first place. Also the conservatism property is satisfied for forcing. Corollary 2.11 a) For any model M P(W) and proposition p it holds In(M) p In(N) p b) For any two models M P(W) and N W such that M N it holds: In(M) h In(N) h The proof uses that if M N then In(M) In(N) which follows from Lemma 2.6; then Lemma 2.10 can be used. Lemma 2.12 For any model N W: In(N) h N h 11
12 Since N In(N) the definition of forcing immediately proves the lemma. 2.4 Verifying a knowledge base Besides defining foundations verification, it is important to be able to actually verify a knowledge base in practice. In this light we should make some remarks about complexity. First of all, there are exponentially many more models in P(W) than there are in W. Therefore, checking inference KB against forcing W will probably be more complicated than checking it against truth. Usually there are many models in W so to compute forcing is time consuming. Moreover, no domain description is considered in the literature. These might be the reasons why verification in the literature has only considered the truth relation. Now there is a problem between forcing, on the one hand as the basis for verification, and on the other hand as the more complicated property to check. A solution is to consider particular illegal constellations of rules that can be proven to violate one of our notions. In the literature this (special case) approach to verification has had a lot of emphasis, mainly because special occurrences of rules are more easily checked than the more difficult notions like soundness, completeness, etc. The following notion describes what the test is that the knowledge base makes for the hypotheses in terms of the observables. It defines a proposition that is induced by a knowledge base for each hypothesis. Definition 2.13 A knowledge base expression of a literal h in OutLit(Ï) is a proposition p in terms of the observables in InLit(Ï) such that h can be deduced from M via KB exactly when p is true in any situation M W : In(M) p ² In(M) KB h In a rule-based system, with chaining as inference relation, this proposition can be found in the form of a disjunction of conjunctions of literals. The disjunction in a sense lists all possible cases (conjunctions) that lead to an hypothesis h. If nothing concludes hypothesis h, then the proposition for that hypothesis h is always false (i.e., an empty disjunction). Example 2.14 Consider a signature < p, q ; r >, and a knowledge base with just two rules KB = { p ª q µ ÅT, Åp µ ÅT }. Then a knowledge base expression for the output literal ÅTis the disjunction ( p ª q) Ó( Åp). Of course, a subtlety arises if some inputs do not arise in a input description. For instance, if Win = { <0,1>, <1,0>, <0,0> } an alternative knowledge base expression is ( Åp) describing the starting point of the only relevant chain. 12
13 If h is an element from OutLit(Ë) then a knowledge base expression will be made not only for h, but for its negation Å h as well. This expression is not necessarily the negation of the proposition p for h. A knowledge base expression is particularly useful when implementing verification of correctness and decisiveness of knowledge bases with respect to domain description, as will be shown in following sections. 3 Consistency and Correctness An important issue in the verification of knowledge-based systems is to assure that the knowledge applied by the system does not derive any contradiction. There are two related notions lying behind this statement. First, we want the knowledge base to be such that it does not derive two conclusions that are inconsistent. Secondly, we want the conclusions to be consistent with the domain we are considering. These two notions are related as will be shown below. 3.1 Consistency A first property that we define here is consistency: we would like inference to be such that one and the same model can never lead to some proposition as well as its negation. If a knowledge base has this property under an inference relation, we call it consistent. Definition 3.1 Given a set of partial models S for a signature Ë, and an inference relation KB. We say that the inference is consistent if for any model M S and proposition p never M KB p and M KB Åp. The common definition of consistency is that two rules (or inferences) are inconsistent if they succeed in the same situation, but have conflicting results. In our view, it misses the point that the input models that lead to these inconsistencies may never occur. Therefore we formulated consistency as a property of the knowledge base with respect to a certain domain description. 3.2 Correctness A system is correct w.r.t. a domain description W when it holds for any specific situation model N W that if an output atom or its negation is inferred from the input information in that situation N, via the KB, then it must also be true in N. This is a notion that is commonly used in the literature of verification. 13
14 Definition 3.2 Assume W is a domain description with respect to a signature Ï, and a knowledge base KB. Then KB is correct with respect to W if for all output literals h OutLit(Ï) the following holds: jn W In(N) KBJ N h Closely related to this is what we call soundness. This checks whether what is derived from the input in an actual situation should indeed follow from that input. In the previous section we described that forcing will be used to set the standards. The main difference with correctness is that we use the forcing relation instead of the satisfaction relation. Definition 3.3 Assume a domain description W with respect to a signature Ï, and KB a knowledge base. Then KB is weakly sound with respect to W if for all output literals h OutLit(Ï) the following holds: jn W In(N) KB h In(N) h. Because an inference can take place also when we have only partial input information about a situation, we will define a second kind of soundness that checks the above property for all possible partial models instead of only the complete models. Definition 3.4 Assume a domain description W with respect to a signature Ï, and a knowledge base KB. Then KB is strongly sound with respect to W if for all output literals h OutLit(Ï) the following holds: jm P(W) In(M) KB h In(M) h The last of the above three definitions seems to be the strongest because it checks all possible partial models instead of only the complete models. Moreover, it checks forcing instead of the simpler holds relation. However, it can be proven that for a knowledge base with a monotonic inference all these notions are equivalent. Theorem 3.5 Let W be a domain description and KB a knowledge base with respect to signature Ë. If the inference relation KB is monotonic with respect to W, then the following are equivalent: (i) KB is strongly sound with respect to W. (ii) KB is weakly sound with respect to W. (iii) KB is correct with respect to W. 14
15 The proof can be found in the Appendix. The notion of correctness (soundness) is related to consistency as defined in Section 3.1. Indeed, if a knowledge base satisfies the weak soundness we can prove consistency. Theorem 3.6 If a knowledge base KB is weakly sound with respect to W, it is also consistent with respect to In(W) and output atoms. The proof runs as follows. If KB is weakly sound we know for any model N W and output atom h OutAt(Ï) that if In(N) KB h andin(n) KB Å h then these two facts together imply In(N) h andin(n) Å h In turn by Lemma 2.12 this impliesn hcpfn Å h This is a contradiction, so KB is consistent with respect to In(W). If a rule set contains rules that lead to contradicting results, the behaviour of the knowledge base is not clear. The final advice the expert system gives will depend on the strategies for selecting rules. It is possible that incorrect conclusions will be drawn. 3.3 Verifying Consistency and Correctness When verifying correctness the notion of rule-based expression turns out useful. Consider the signature Ï = < s 1, s 2, s 3, s 4, s 5 ; i 1 ; h 1, h 2 > and the domain description W given by: N 1 = < 1, 0, 1, 0, 0 ; 1 ; 1, 0 > N 2 = < 1, 0, 0, 1, 0 ; 1 ; 0, 1 > N 3 = < 0, 1, 0, 0, 1 ; 0 ; 1, 0 > that was reasoned about by the KB with rules: s 1 ª Å s 2 µ i 1 Å s 5 µ i 1 i 1 ª s 3 µ h 1 i 1 ª s 4 µ h 2 Correctness can be established by considering all possible inferences to hypotheses. For example, because In(N 1 ) s 1 ª Å s 2 it allows the chain s 1 ª Å s 2 µ i 1 ; i 1 ª s 3 µ h 1 Thus h 1 can be inferred by KB, and therefore In(N 1 ) KB h 1. Correctness is obeyed, because N 1 h 1. No other inference chain leads to an output from In(N 1 ). Because we do not assume the closed-world assumption we cannot derive (by failure) any negations of hypotheses. Next, In(N 2 ) allows the chain s 1 ª Å s 2 µ i 1 ; i 1 ª s 4 µ h 2, so In(N 2 ) KB h 2. There is no 15
16 incorrectness because N 2 h 2. Finally, In(N 3 ) allows nothing to be inferred via the KB, so correctness holds automatically here. A program can check the knowledge base expressions (see Definition 2.13) of every hypothesiscpfkvupgicvkqp+pvjkuyc[kvkugcu[vqejgemyjgvjgtgiin(n 1 ) infers h1 by taking the proposition p associated with h1, and checking whether In(N 1 ) makes p true. If so, then check whether N 1 h 1. Do this for every hypothesis and its negation, i.e. do it for every proposition that has been built. The following lemma allows one to easily check for correctness in this way. Lemma 3.7 Let p be the knowledge base expression for a literal hfrom OutLit(Ï. If all models N W such that In(N) p also satisfy N h then KB KUEQTTGEVYKVJTGURGEVVQW. There is no need to check weak and strong soundness once correctness has been checked, because (assuming the inference relation is monotonic) they are equivalent by Theorem 3.5. Lemma 3.8 If all rules r in KB are true in all models of W, then KB KUEQTTGEVYKVJTGURGEVVQW. Another way to verify correctness is given in the above lemma. It is possible to check whether each rule of KB is true in all models of W. This follows as one can easily show that then any chain of rules that is true in a model, provides a conclusion that is true in that model too. By Theorem 3.6 we have then automatically checked consistency. The literature considers several special cases of rules that make a knowledge base inconsistent. Some of these are self-contradicting rules and rule-chains, and more important, contradicting pairs of rules and rule-chains. The first two cases, those of self-contradicting antecedents in rules and rule-chains, are not consistency in the semantic sense. They will be considered as a case of redundancy later. self-contradicting rule: This is a rule which contradicts itself and of which the negation of its conclusion occurs in its antecedent. For example, p ª q µ ÅR. self-contradicting chain of inference: Same as above, but the contradiction does not occur until after some inferences. For example, p ª q µ r ; r ª s µ ÅR. 16
17 If they occur in reasoning sessions, these examples are shown to be special cases of our definition of inconsistency as follows. For ÅR to be inferred, p has to be true (in both examples); so, In(N) KB p. Now assume (considering both examples) q and s (in the second example) are in In(N), then In(N) KB Å p, and the inconsistency follows. For self-contradicting inferences it is checked if the conditions that have to be true to derive the contradiction are ever true simultaneously in a model. When all the conditions of a rule or chain are input literals then the contradiction is easily verified in the models. However, if one of these conditions contains an internal literal, it is somewhat more difficult to see if the internal literal is true for a model. This is because internal literals are not specified in models (only input and output literals). To check the truth value of an internal literal in a model, it is checked if the observables in one of the models together with the rules from the KB infer the internal literal. When all conditions, that have to be true to infer a contradiction, are true in the model (input and internal literals), the contradiction is also implied by the model. contradicting rule-pair: This is the case when two rules succeed with the same antecedent, but with conflicting conclusions. For example, p ª q µ s; p ª q µ Ås. contradicting chain of inference: Same as above, but the contradiction happens after some inferences. For example, p µ q ; q µ r and p µ s ; s µ ÅT. Note that verifying contradicting rules can lead to an extra possibility of contradiction, one that is not considered when checking without a domain description. In a model a conflict can not only occur when two rules or chains of rules with conflicting conclusions have equivalent conditions, but additionally conflicts occur for rules with different conditions and conflicting conclusions. For example, consider the following rules: p ª ÅS µ s, and p ª r µ Ås. Without a domain description the conflict is not detected, but a conflict arises in a model if p, ÅS, and r are true simultaneously. If no such model exists in the domain there is no inconsistency. These examples are special cases of our definition of inconsistency too. Take for example the two rules from contradicting rule-pairs: p ª q µ s; p ª q µ Ås. Apply the definition of consistency and one can see In(N) KB s and In(N) KBÅs where In(N) is the input part of model N, here based on p and q. 4 Weak Completeness and Gaps in the Knowledge Base The development of a knowledge-based system is an iterative process in which knowledge is tested, added, changed, and refined. This iterative process can leave gaps in the knowledge base, which both the knowledge engineer and the expert may have overlooked during the knowledge acquisition process. 17
18 In the previous section the direction of verification was from the knowledge base back to the world. For any derivation it was checked whether it violated any criteria set by the world. In this section the direction will be reversed, and the idea is that the standards as set by the world must be achieved by the inferences. In general this is called completeness; as will turn out in this and subsequent sections three different types of completeness can be defined. The gaps or missing rules may or may not be easy to detect, but they usually indicate that an intended derivation is not possible. This incompleteness may be intentional or not; intentionally missing rules relate to those cases where the omitted rules do not have any bearing on the task at hand. Unintentionally missing rules are a result of omissions in the development process. 4.1 Weak Completeness Usually incompleteness is indicated by a gap or missing rule. If a hypothesis should be derivable from an input model, possibly because it holds in a situation with that input, but a derivation of that hypothesis cannot be performed then there may be some missing rules. Suwa et al. [31] have informally defined missing rules as follows: "A situation exists in which a particular inference is required, but there is no rule that succeeds in that situation and produces the desired conclusion." Such a definition is based on a knowledge base in a certain format. But what it does in essence is to capture a relation between a desired conclusion and a particular inference. In our formalism this can be defined as a relation between forcing and inference KB as in the following definition. Definition 4.1 Assume a domain description W with respect to a signature Ï, and a knowledge base KB. Then KB is weakly complete with respect to W if for all output literals h OutLit(Ï) the following holds: jn W In(N) h In(N) KB J Note that weak completeness is the converse of weak soundness. These two notions, soundness and weak completeness show the essence of verification as described here. They show most clearly the comparison between forcing and inference. Where the notions of correctness and soundness w.r.t. a domain description were shown to be equivalent, the notions of (weak/strong) completeness and decisiveness (as will be defined in subsequent sections) are not equivalent. They are, however, if some additional properties of the knowledge base and domain description are satisfied (i.e., well-informedness and empirically foundedness, introduced in Section 5 and 6). Consider the following example again. 18
19 W: N 1 = < 1, 0, 1, 0, 0 ; 1 ; 1, 0 > N 2 = < 1, 0, 0, 1, 0 ; 1 ; 0, 1 > N 3 = < 0, 1, 0, 0, 1 ; 0 ; 1, 0 > s 1 ª Å s 2 µ i 1 Å s 5 µ i 1 i 1 ª s 3 µ h 1 i 1 ª s 4 µ h 2 The knowledge base in the example is not weakly complete because the input of N 2 forces Åh 1, and the inputs of N 1 and N 3 both force Åh 2. These hypotheses are not inferred from the appropriate inputs, for the simple reason that there is no rule that contains these literals as its conclusion. We should add rules like s 4 µ Å h 1 and Å s 4 µ Å h 2 to make the knowledge base weakly complete with respect to W. 4.2 Gaps in the knowledge base Checking for weak completeness can be complex mainly because forcing is a complicated notion. In line with the literature, we have identified five cases indicative of gaps (incomplete information): unnecessary literals, dead ends, unreachable literals, unreachable rules, and illegal literals. The main intuition behind these special cases is that the occurrence of an atom in the signature indicates that the atom is needed to determine (it helps to force) the truth of some hypothesis in some situation. An atom a is essential for the forcing of an output literal h if any model that forces h either assigns unknown to a or its sub model with unknown assigned to a does not force h. We will try to show that the cases below can be seen as special cases of failure of weak completeness. * Unnecessary literals A literal that is mentioned in the input signature is unnecessary if it is not mentioned in any rule, neither in the antecedent nor in the conclusion, and if it is not mentioned in the output. In the latter case, the literal can have a value through interaction with other components and pass that value on. Then an input literal is necessary even if it does not occur as an antecedent of any rule, and an output literal is necessary even if it does not occur as a conclusion of any rule. For example suppose we have the relation problem with the set of legal values (inputobjects) {cd_dirty, cd_upside_down, power_off}. If problem(cd_dirty) and problem(cd_upside_down) 19
20 occur in the antecedent of a rule in the knowledge base, but problem(power_off) does not, and problem(power_off) does not occur in the output signature then either the knowledge base is a rule short or the atom can be deleted from the input signature. This can be seen as a special case of failure of weak completeness. Suppose there is a model N, with the literal s in it, that forces an output h (so In(N) W h), and the output h cannot be inferred from In(N) and the knowledge base (i.e., In(N)ÁKB h. This is because there is no rule that uses the literal s in question as part of its condition. So weak completeness does not hold, and there is a missing rule. Then again, if the literal in question is not used in any model to force h then it is unnecessary. * Illegal literals This is the case when a rule refers to a literal that does not occur in any signature. For example, problem(power_off) occurs in a rule s antecedent but does not occur in the input or internal signature. The same holds for output literals. Some conclusion is drawn by a rule in the knowledge base, but that conclusion is not part of the output signature nor is it part of the internal signature. Conditions are not allowed to come from the output signature, unless they are declared in the input signature as well. In the same way, conclusions can only be input literals in they are declared in the output signature as well. Actually, the occurrence of illegal literals is not really part of weak completeness, but it is more a declaration error. This part is actually a kind of syntax checker as well: if one misspells something, like problem(cd_dirty), then this is determined to be an illegal literal, because problem(cd_dirty) is the right input literal. Illegal literals in models are values which are declared in the modelsfile, but which are not declared in the signatures of the component. * Dead-ends A dead end occurs in an inference chain if a fact, that is not an output, is concluded and does not form a part of the antecedents of any other rule. So q is a dead end, if in the rule p µ q, the literal q is no output and is no part of the antecedents of any other rule. A dead-end related to a model occurs when from the observables of a model via the KB the dead-end can be inferred. * Unreachable rules A rule is not reachable if one of its conditions is not concluded in any rule, and is not an input literal. This means that the rule will never be used in a chain. Unreachability of rules does not depend on whether or not a domain description is considered. 20
CHAPTER 7 GENERAL PROOF SYSTEMS 1 Introduction Proof systems are built to prove statements. They can be thought as an inference machine with special statements, called provable statements, or sometimesMore information
Chapter II. Controlling Cars on a Bridge
Chapter II. Controlling Cars on a Bridge 1 Introduction The intent of this chapter is to introduce a complete example of a small system development. During this development, you will be made aware of theMore information
A terminology model approach for defining and managing statistical metadata
A terminology model approach for defining and managing statistical metadata Comments to : R. Karge (49) 30-6576 2791 mail firstname.lastname@example.com Content 1 Introduction... 4 2 Knowledge presentation...More information
KNOWLEDGE FACTORING USING NORMALIZATION THEORY J. VANTHIENEN M. SNOECK Katholieke Universiteit Leuven Department of Applied Economic Sciences Dekenstraat 2, 3000 Leuven (Belgium) tel. (+32) 16 28 58 09More information
Logic in general. Inference rules and theorem proving
Logical Agents Knowledge-based agents Logic in general Propositional logic Inference rules and theorem proving First order logic Knowledge-based agents Inference engine Knowledge base Domain-independentMore information
Mathematics for Computer Science/Software Engineering. Notes for the course MSM1F3 Dr. R. A. Wilson
Mathematics for Computer Science/Software Engineering Notes for the course MSM1F3 Dr. R. A. Wilson October 1996 Chapter 1 Logic Lecture no. 1. We introduce the concept of a proposition, which is a statementMore information
CHAPTER 3. Methods of Proofs. 1. Logical Arguments and Formal Proofs
CHAPTER 3 Methods of Proofs 1. Logical Arguments and Formal Proofs 1.1. Basic Terminology. An axiom is a statement that is given to be true. A rule of inference is a logical rule that is used to deduceMore information
Handout #1: Mathematical Reasoning
Math 101 Rumbos Spring 2010 1 Handout #1: Mathematical Reasoning 1 Propositional Logic A proposition is a mathematical statement that it is either true or false; that is, a statement whose certainty orMore information
Coverability for Parallel Programs
2015 http://excel.fit.vutbr.cz Coverability for Parallel Programs Lenka Turoňová* Abstract We improve existing method for the automatic verification of systems with parallel running processes. The techniqueMore information
Reusable Knowledge-based Components for Building Software. Applications: A Knowledge Modelling Approach
Reusable Knowledge-based Components for Building Software Applications: A Knowledge Modelling Approach Martin Molina, Jose L. Sierra, Jose Cuena Department of Artificial Intelligence, Technical UniversityMore information
Access Control Models Part I. Murat Kantarcioglu UT Dallas
UT DALLAS Erik Jonsson School of Engineering & Computer Science Access Control Models Part I Murat Kantarcioglu UT Dallas Introduction Two main categories: Discretionary Access Control Models (DAC) Definition:More information
Determination of the normalization level of database schemas through equivalence classes of attributes
Computer Science Journal of Moldova, vol.17, no.2(50), 2009 Determination of the normalization level of database schemas through equivalence classes of attributes Cotelea Vitalie Abstract In this paper,More information
A Propositional Dynamic Logic for CCS Programs
A Propositional Dynamic Logic for CCS Programs Mario R. F. Benevides and L. Menasché Schechter {mario,firstname.lastname@example.com Abstract This work presents a Propositional Dynamic Logic in which the programs areMore information
Correspondence analysis for strong three-valued logic
Correspondence analysis for strong three-valued logic A. Tamminga abstract. I apply Kooi and Tamminga s (2012) idea of correspondence analysis for many-valued logics to strong three-valued logic (K 3 ).More information
facultad de informática universidad politécnica de madrid
facultad de informática universidad politécnica de madrid On the Confluence of CHR Analytical Semantics Rémy Haemmerlé Universidad olitécnica de Madrid & IMDEA Software Institute, Spain TR Number CLI2/2014.0More information
CS510 Software Engineering
CS510 Software Engineering Propositional Logic Asst. Prof. Mathias Payer Department of Computer Science Purdue University TA: Scott A. Carr Slides inspired by Xiangyu Zhang http://nebelwelt.net/teaching/15-cs510-seMore information
WHAT ARE MATHEMATICAL PROOFS AND WHY THEY ARE IMPORTANT? introduction Many students seem to have trouble with the notion of a mathematical proof. People that come to a course like Math 216, who certainlyMore information
2. Methods of Proof Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try.
2. METHODS OF PROOF 69 2. Methods of Proof 2.1. Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try. Trivial Proof: If we know q is true thenMore information
Critical and creative thinking (higher order thinking) refer to a set of cognitive skills or strategies that increases the probability of a desired outcome. In an information- rich society, the qualityMore information
Computational Methods for Database Repair by Signed Formulae
Computational Methods for Database Repair by Signed Formulae Ofer Arieli (firstname.lastname@example.com) Department of Computer Science, The Academic College of Tel-Aviv, 4 Antokolski street, Tel-Aviv 61161, Israel.More information
Overview of the TACITUS Project
Overview of the TACITUS Project Jerry R. Hobbs Artificial Intelligence Center SRI International 1 Aims of the Project The specific aim of the TACITUS project is to develop interpretation processes forMore information
MATH10212 Linear Algebra. Systems of Linear Equations. Definition. An n-dimensional vector is a row or a column of n numbers (or letters): a 1.
MATH10212 Linear Algebra Textbook: D. Poole, Linear Algebra: A Modern Introduction. Thompson, 2006. ISBN 0-534-40596-7. Systems of Linear Equations Definition. An n-dimensional vector is a row or a columnMore information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
3. Mathematical Induction
3. MATHEMATICAL INDUCTION 83 3. Mathematical Induction 3.1. First Principle of Mathematical Induction. Let P (n) be a predicate with domain of discourse (over) the natural numbers N = {0, 1,,...}. If (1)More information
NP-Completeness and Cook s Theorem
NP-Completeness and Cook s Theorem Lecture notes for COM3412 Logic and Computation 15th January 2002 1 NP decision problems The decision problem D L for a formal language L Σ is the computational task:More information
Introducing Formal Methods. Software Engineering and Formal Methods
Introducing Formal Methods Formal Methods for Software Specification and Analysis: An Overview 1 Software Engineering and Formal Methods Every Software engineering methodology is based on a recommendedMore information
Degrees of Truth: the formal logic of classical and quantum probabilities as well as fuzzy sets.
Degrees of Truth: the formal logic of classical and quantum probabilities as well as fuzzy sets. Logic is the study of reasoning. A language of propositions is fundamental to this study as well as trueMore information
Generating models of a matched formula with a polynomial delay
Generating models of a matched formula with a polynomial delay Petr Savicky Institute of Computer Science, Academy of Sciences of Czech Republic, Pod Vodárenskou Věží 2, 182 07 Praha 8, Czech RepublicMore information
Improving Knowledge-Based System Performance by Reordering Rule Sequences
Improving Knowledge-Based System Performance by Reordering Rule Sequences Neli P. Zlatareva Department of Computer Science Central Connecticut State University 1615 Stanley Street New Britain, CT 06050More information
M.Sc. program in mathematics INTRODUCTORY SET THEORY Katalin Károlyi Department of Applied Analysis, Eötvös Loránd University H-1088 Budapest, Múzeum krt. 6-8. CONTENTS 1. SETS Set, equal sets, subset,More information
A first step towards modeling semistructured data in hybrid multimodal logic
A first step towards modeling semistructured data in hybrid multimodal logic Nicole Bidoit * Serenella Cerrito ** Virginie Thion * * LRI UMR CNRS 8623, Université Paris 11, Centre d Orsay. ** LaMI UMRMore information
Formal Engineering for Industrial Software Development
Shaoying Liu Formal Engineering for Industrial Software Development Using the SOFL Method With 90 Figures and 30 Tables Springer Contents Introduction 1 1.1 Software Life Cycle... 2 1.2 The Problem 4 1.3More information
136 TER 4. INDUCTION, GRHS ND TREES 4.3 Graphs In this chapter we introduce a fundamental structural idea of discrete mathematics, that of a graph. Many situations in the applications of discrete mathematicsMore information
CHANCE ENCOUNTERS. Making Sense of Hypothesis Tests. Howard Fincher. Learning Development Tutor. Upgrade Study Advice Service
CHANCE ENCOUNTERS Making Sense of Hypothesis Tests Howard Fincher Learning Development Tutor Upgrade Study Advice Service Oxford Brookes University Howard Fincher 2008 PREFACE This guide has a restrictedMore information
Problems often have a certain amount of uncertainty, possibly due to: Incompleteness of information about the environment,
Uncertainty Problems often have a certain amount of uncertainty, possibly due to: Incompleteness of information about the environment, E.g., loss of sensory information such as vision Incorrectness inMore information
Predicate Calculus. There are certain arguments that seem to be perfectly logical, yet they cannot be expressed by using propositional calculus.
Predicate Calculus (Alternative names: predicate logic, first order logic, elementary logic, restricted predicate calculus, restricted functional calculus, relational calculus, theory of quantification,More information
Introduction to Logic in Computer Science: Autumn 2006
Introduction to Logic in Computer Science: Autumn 2006 Ulle Endriss Institute for Logic, Language and Computation University of Amsterdam Ulle Endriss 1 Plan for Today Now that we have a basic understandingMore information
Computing and Informatics, Vol. 20, 2001,????, V 2006-Nov-6 UPDATES OF LOGIC PROGRAMS Ján Šefránek Department of Applied Informatics, Faculty of Mathematics, Physics and Informatics, Comenius University,More information
Testing LTL Formula Translation into Büchi Automata
Testing LTL Formula Translation into Büchi Automata Heikki Tauriainen and Keijo Heljanko Helsinki University of Technology, Laboratory for Theoretical Computer Science, P. O. Box 5400, FIN-02015 HUT, FinlandMore information
Specification and Analysis of Contracts Lecture 1 Introduction
Specification and Analysis of Contracts Lecture 1 Introduction Gerardo Schneider email@example.com http://folk.uio.no/gerardo/ Department of Informatics, University of Oslo SEFM School, Oct. 27 - Nov.More information
Mathematical Induction
Mathematical Induction In logic, we often want to prove that every member of an infinite set has some feature. E.g., we would like to show: N 1 : is a number 1 : has the feature Φ ( x)(n 1 x! 1 x) HowMore information
Computational Logic in an Object-Oriented World
Computational Logic in an Object-Oriented World Robert Kowalski Imperial College London firstname.lastname@example.com Abstract Logic and object-orientation (OO) are competing ways of looking at the world. Both viewMore information
Likewise, we have contradictions: formulas that can only be false, e.g. (p p).
CHAPTER 4. STATEMENT LOGIC 59 The rightmost column of this truth table contains instances of T and instances of F. Notice that there are no degrees of contingency. If both values are possible, the formulaMore information
On the Relationship between Classes P and NP
Journal of Computer Science 8 (7): 1036-1040, 2012 ISSN 1549-3636 2012 Science Publications On the Relationship between Classes P and NP Anatoly D. Plotnikov Department of Computer Systems and Networks,More information
Research Note. Bi-intuitionistic Boolean Bunched Logic
UCL DEPARTMENT OF COMPUTER SCIENCE Research Note RN/14/06 Bi-intuitionistic Boolean Bunched Logic June, 2014 James Brotherston Dept. of Computer Science University College London Jules Villard Dept. ofMore information
Problem Set I: Preferences, W.A.R.P., consumer choice
Problem Set I: Preferences, W.A.R.P., consumer choice Paolo Crosetto email@example.com Exercises solved in class on 18th January 2009 Recap:,, Definition 1. The strict preference relation is x yMore information
2. Basic Relational Data Model
2. Basic Relational Data Model 2.1 Introduction Basic concepts of information models, their realisation in databases comprising data objects and object relationships, and their management by DBMS s thatMore information
Simulation-Based Security with Inexhaustible Interactive Turing Machines
Simulation-Based Security with Inexhaustible Interactive Turing Machines Ralf Küsters Institut für Informatik Christian-Albrechts-Universität zu Kiel 24098 Kiel, Germany email@example.com information
Scalable Automated Symbolic Analysis of Administrative Role-Based Access Control Policies by SMT solving
Scalable Automated Symbolic Analysis of Administrative Role-Based Access Control Policies by SMT solving Alessandro Armando 1,2 and Silvio Ranise 2, 1 DIST, Università degli Studi di Genova, Italia 2 SecurityMore information
The Foundations: Logic and Proofs. Chapter 1, Part III: Proofs
The Foundations: Logic and Proofs Chapter 1, Part III: Proofs Rules of Inference Section 1.6 Section Summary Valid Arguments Inference Rules for Propositional Logic Using Rules of Inference to Build ArgumentsMore information
Subsets of Euclidean domains possessing a unique division algorithm
Subsets of Euclidean domains possessing a unique division algorithm Andrew D. Lewis 2009/03/16 Abstract Subsets of a Euclidean domain are characterised with the following objectives: (1) ensuring uniquenessMore information
Integrating Benders decomposition within Constraint Programming
Integrating Benders decomposition within Constraint Programming Hadrien Cambazard, Narendra Jussien email: {hcambaza,email@example.com École des Mines de Nantes, LINA CNRS FRE 2729 4 rue Alfred Kastler BPMore information
A Logic Approach for LTL System Modification
A Logic Approach for LTL System Modification Yulin Ding and Yan Zhang School of Computing & Information Technology University of Western Sydney Kingswood, N.S.W. 1797, Australia email: {yding,firstname.lastname@example.com information
Information Technology Security Evaluation Criteria. ITSEC Joint Interpretation Library (ITSEC JIL)
S Information Technology Security Evaluation Criteria ITSEC Joint Interpretation Library (ITSEC JIL) Version 2.0 November 1998 This document is paginated from i to vi and from 1 to 65 ITSEC Joint InterpretationMore information
Z Styles for Security Properties and Modern User Interfaces
Z Styles for Security Properties and Modern User Interfaces Anthony Hall Praxis Critical Systems, 20 Manvers Street, Bath BA1 1PX firstname.lastname@example.com Abstract. This paper describes two new stylesMore information
Artificial Intelligence
Artificial Intelligence ICS461 Fall 2010 1 Lecture #12B More Representations Outline Logics Rules Frames Nancy E. Reed firstname.lastname@example.com 2 Representation Agents deal with knowledge (data) Facts (believeMore information
PROCEEDINGS OF THE YEREVAN STATE UNIVERSITY Physical and Mathematical Sciences 2012 1 p. 43 48 ON FUNCTIONAL SYMBOL-FREE LOGIC PROGRAMS I nf or m at i cs L. A. HAYKAZYAN * Chair of Programming and InformationMore information
Neighborhood Data and Database Security
Neighborhood Data and Database Security Kioumars Yazdanian, FrkdCric Cuppens e-mail: yaz@ tls-cs.cert.fr - cuppens@ tls-cs.cert.fr CERT / ONERA, Dept. of Computer Science 2 avenue E. Belin, B.P. 4025,31055More information
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic Lars Birkedal Rasmus Ejlers Møgelberg Rasmus Lerchedahl Petersen IT University Technical Report Series TR-00-7 ISSN 600 600 February 00More information
Integrating Pattern Mining in Relational Databases
Integrating Pattern Mining in Relational Databases Toon Calders, Bart Goethals, and Adriana Prado University of Antwerp, Belgium {toon.calders, bart.goethals, email@example.com Abstract. Almost aMore information
Lecture 9 - Message Authentication Codes
Lecture 9 - Message Authentication Codes Boaz Barak March 1, 2010 Reading: Boneh-Shoup chapter 6, Sections 9.1 9.3. Data integrity Until now we ve only been interested in protecting secrecy of data. However,More information
OPERATIONAL TYPE THEORY by Adam Petcher Prepared under the direction of Professor Aaron Stump A thesis presented to the School of Engineering of
WASHINGTON NIVERSITY SCHOOL OF ENGINEERING AND APPLIED SCIENCE DEPARTMENT OF COMPTER SCIENCE AND ENGINEERING DECIDING JOINABILITY MODLO GROND EQATIONS IN OPERATIONAL TYPE THEORY by Adam Petcher PreparedMore information
Removing Partial Inconsistency in Valuation- Based Systems*
Removing Partial Inconsistency in Valuation- Based Systems* Luis M. de Campos and Serafín Moral Departamento de Ciencias de la Computación e I.A., Universidad de Granada, 18071 Granada, Spain This paperMore information
Virtual Time and Timeout in Client-Server Networks
Virtual Time and Timeout in Client-Server Networks Jayadev Misra July 13, 2011 Contents 1 Introduction 2 1.1 Background.............................. 2 1.1.1 Causal Model of Virtual Time...............More information
! " # The Logic of Descriptions. Logics for Data and Knowledge Representation. Terminology. Overview. Three Basic Features. Some History on DLs
,!0((,.+#$),%$(-&.& *,2(-$)%&2.'3&%!&, Logics for Data and Knowledge Representation Alessandro Agostini email@example.com University of Trento Fausto Giunchiglia firstname.lastname@example.com The Logic of Descriptions!$%&'()*$#)More information
A three-dimensional visualization of communications in distributed program environments
Engineering Industrial & Management Engineering fields Okayama University Year 2003 A three-dimensional visualization of communications in distributed program environments Mariko Sasakura Okayama UniversityMore information
Draft Martin Doerr ICS-FORTH, Heraklion, Crete Oct 4, 2001
A comparison of the OpenGIS TM Abstract Specification with the CIDOC CRM 3.2 Draft Martin Doerr ICS-FORTH, Heraklion, Crete Oct 4, 2001 1 Introduction This Mapping has the purpose to identify, if the OpenGISMore information
Fuzzy Implication Rules. Adnan Yazıcı Dept. of Computer Engineering, Middle East Technical University Ankara/Turkey
Fuzzy Implication Rules Adnan Yazıcı Dept. of Computer Engineering, Middle East Technical University Ankara/Turkey Fuzzy If-Then Rules Remember: The difference between the semantics of fuzzy mapping rulesMore information
Random vs. Structure-Based Testing of Answer-Set Programs: An Experimental Comparison
Random vs. Structure-Based Testing of Answer-Set Programs: An Experimental Comparison Tomi Janhunen 1, Ilkka Niemelä 1, Johannes Oetsch 2, Jörg Pührer 2, and Hans Tompits 2 1 Aalto University, DepartmentMore information
13 Infinite Sets. 13.1 Injections, Surjections, and Bijections. mcs-ftl 2010/9/8 0:40 page 379 #385
mcs-ftl 2010/9/8 0:40 page 379 #385 13 Infinite Sets So you might be wondering how much is there to say about an infinite set other than, well, it has an infinite number of elements. Of course, an infiniteMore information
Introduction to knowledge representation and reasoning. We now look briefly at how knowledge about the world might be represented and reasoned with.
Introduction to knowledge representation and reasoning We now look briefly at how knowledge about the world might be represented and reasoned with. Aims: To introduce semantic networks and frames for knowledgeMore information
Lehrstuhl für Informatik 2
Analytical Learning Introduction Lehrstuhl Explanation is used to distinguish the relevant features of the training examples from the irrelevant ones, so that the examples can be generalised IntroductionMore information
The epistemic structure of de Finetti s betting problem
The epistemic structure of de Finetti s betting problem Tommaso Flaminio 1 and Hykel Hosni 2 1 IIIA - CSIC Campus de la Univ. Autònoma de Barcelona s/n 08193 Bellaterra, Spain. Email: firstname.lastname@example.com information
THE FUNDAMENTAL THEOREM OF ARBITRAGE PRICING 1. Introduction The Black-Scholes theory, which is the main subject of this course and its sequel, is based on the Efficient Market Hypothesis, that arbitragesMore information
Partitioning edge-coloured complete graphs into monochromatic cycles and paths
arxiv:1205.5492v1 [math.co] 24 May 2012 Partitioning edge-coloured complete graphs into monochromatic cycles and paths Alexey Pokrovskiy Departement of Mathematics, London School of Economics and PoliticalMore information
Unraveling versus Unraveling: A Memo on Competitive Equilibriums and Trade in Insurance Markets
Unraveling versus Unraveling: A Memo on Competitive Equilibriums and Trade in Insurance Markets Nathaniel Hendren January, 2014 Abstract Both Akerlof (1970) and Rothschild and Stiglitz (1976) show thatMore information
The Role of Dispute Settlement Procedures in International Trade Agreements: Online Appendix
The Role of Dispute Settlement Procedures in International Trade Agreements: Online Appendix Giovanni Maggi Yale University, NBER and CEPR Robert W. Staiger Stanford University and NBER November 2010 1.More information
- 1-8. KNOWLEDGE BASED SYSTEMS IN MANUFACTURING SIMULATION 8.1 Introduction 8.1.1 Summary introduction The first part of this section gives a brief overview of some of the different uses of expert systemsMore information
OHJ-2306 Introduction to Theoretical Computer Science, Fall 2012 8.11.2012
276 The P vs. NP problem is a major unsolved problem in computer science It is one of the seven Millennium Prize Problems selected by the Clay Mathematics Institute to carry a $ 1,000,000 prize for theMore information
University of Ostrava. Reasoning in Description Logic with Semantic Tableau Binary Trees
University of Ostrava Institute for Research and Applications of Fuzzy Modeling Reasoning in Description Logic with Semantic Tableau Binary Trees Alena Lukasová Research report No. 63 2005 Submitted/toMore information
Software Verification and Testing. Lecture Notes: Z I
Software Verification and Testing Lecture Notes: Z I Motivation so far: we have seen that properties of software systems can be specified using first-order logic, set theory and the relational calculusMore information
SOLUTIONS TO ASSIGNMENT 1 MATH 576 SOLUTIONS BY OLIVIER MARTIN 13 #5. Let T be the topology generated by A on X. We want to show T = J B J where B is the set of all topologies J on X with A J. This amountsMore information
Finite Sets. Theorem 5.1. Two non-empty finite sets have the same cardinality if and only if they are equivalent.
MATH 337 Cardinality Dr. Neal, WKU We now shall prove that the rational numbers are a countable set while R is uncountable. This result shows that there are two different magnitudes of infinity. But weMore information
On strong fairness in UNITY
On strong fairness in UNITY H.P.Gumm, D.Zhukov Fachbereich Mathematik und Informatik Philipps Universität Marburg {gumm,email@example.com Abstract. In [6] Tsay and Bagrodia present a correctMore information
6.080/6.089 GITCS Feb 12, 2008. Lecture 3
6.8/6.89 GITCS Feb 2, 28 Lecturer: Scott Aaronson Lecture 3 Scribe: Adam Rogal Administrivia. Scribe notes The purpose of scribe notes is to transcribe our lectures. Although I have formal notes of myMore information
Data Validation with OWL Integrity Constraints
Data Validation with OWL Integrity Constraints (Extended Abstract) Evren Sirin Clark & Parsia, LLC, Washington, DC, USA email@example.com Abstract. Data validation is an important part of data integrationMore information
Chapter 21: The Discounted Utility Model
Chapter 21: The Discounted Utility Model 21.1: Introduction This is an important chapter in that it introduces, and explores the implications of, an empirically relevant utility function representing intertemporalMore information
each college c i C has a capacity q i - the maximum number of students it will admit
n colleges in a set C, m applicants in a set A, where m is much larger than n. each college c i C has a capacity q i - the maximum number of students it will admit each college c i has a strict order iMore information
Automated Theorem Proving - summary of lecture 1
Automated Theorem Proving - summary of lecture 1 1 Introduction Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement is a logical consequence ofMore information
Monitoring Metric First-order Temporal Properties
Monitoring Metric First-order Temporal Properties DAVID BASIN, FELIX KLAEDTKE, SAMUEL MÜLLER, and EUGEN ZĂLINESCU, ETH Zurich Runtime monitoring is a general approach to verifying system properties atMore information
Updating Action Domain Descriptions
Updating Action Domain Descriptions Thomas Eiter, Esra Erdem, Michael Fink, and Ján Senko Institute of Information Systems, Vienna University of Technology, Vienna, Austria Email: (eiter esra michael jan)@kr.tuwien.ac.atMore information
Factoring & Primality
Factoring & Primality Lecturer: Dimitris Papadopoulos In this lecture we will discuss the problem of integer factorization and primality testing, two problems that have been the focus of a great amountMore information
Verifying Semantic of System Composition for an Aspect-Oriented Approach
2012 International Conference on System Engineering and Modeling (ICSEM 2012) IPCSIT vol. 34 (2012) (2012) IACSIT Press, Singapore Verifying Semantic of System Composition for an Aspect-Oriented ApproachMore information
The Classes P and NP
The Classes P and NP We now shift gears slightly and restrict our attention to the examination of two families of problems which are very important to computer scientists. These families constitute theMore information
EMBEDDING COUNTABLE PARTIAL ORDERINGS IN THE ENUMERATION DEGREES AND THE ω-enumeration DEGREES MARIYA I. SOSKOVA AND IVAN N. SOSKOV 1. Introduction One of the most basic measures of the complexity of aMore information
Chapter 7 Application Protocol Reference Architecture
Application Protocol Reference Architecture Chapter 7 Application Protocol Reference Architecture This chapter proposes an alternative reference architecture for application protocols. The proposed referenceMore information
(LMCS, p. 317) V.1. First Order Logic. This is the most powerful, most expressive logic that we will examine.
(LMCS, p. 317) V.1 First Order Logic This is the most powerful, most expressive logic that we will examine. Our version of first-order logic will use the following symbols: variables connectives (,,,,More information
2. The Language of First-order Logic
2. The Language of First-order Logic KR & R Brachman & Levesque 2005 17 Declarative language Before building system before there can be learning, reasoning, planning, explanation... need to be able toMore information
Which Semantics for Neighbourhood Semantics?
Which Semantics for Neighbourhood Semantics? Carlos Areces INRIA Nancy, Grand Est, France Diego Figueira INRIA, LSV, ENS Cachan, France Abstract In this article we discuss two alternative proposals forMore information
Linear Codes. Chapter 3. 3.1 Basics
Chapter 3 Linear Codes In order to define codes that we can encode and decode efficiently, we add more structure to the codespace. We shall be mainly interested in linear codes. A linear code of lengthMore information


text:
$ 70.00
Get the classic 1950s look with this birdcage style embellished veil.
Made in: NEW
Made of: tulle, pearls
Color: blush
Hair Adornment Suggestions:
items left
Bridal Accessories
$ 150.00
Rare lace cap with hand beaded decorative front & wax flowers.
Made In: 1920
Made of: lace, beads
Color: ivory
Veil Style Suggestions:
View full product details →
item left
Subscribe to our newsletter and always be the first to hear about what is happening.
Shopping Cart by Shopify

subset: commoncrawl


text:
Duration: 149min 00sec Views: 16 863 Submitted: 1 year ago Submitted by:
Description: This sensual video explores lesbian lovemaking like no other adult video has before. No phony acting, youll watch five well-endowed all-girl couples reveal every intimate of what women really want. This video includes Heidi Hooters, Trinity Loren, Tracy Gibb and Anita. Also Donna Ambrose and Justine go pussy to pussy, and Jeannine Oldfield casts off her inhibitions in a spirited lesbian tryst with Vietta.
Tags: Voluptuous Lesbian Adultery Lovers Knockers


text:
Hiring HVAC mechanics and helpers!
April 24, 2013
With the expansion of our HVAC division we are searching for experienced and reliable individuals. Needs to have experience with sheet metal. For more information please apply at our Rehoboth Beach location in the Midway Shopping Center.
Calendar of Events
- Today
- Saturday, July 29
- Sunday, July 30


text:
Top Ten Most Pointless Star Wars CharactersCaptainComedy17
The Contenders: Page 5
Ahsoka is just awesome...when she was kicked out of the Jedi order we saw how it really angered anakin...that was just another step towards his fall to the dark side
Super pointless.
Second pointless in all the starwars. First is Rey of course.
She was the chosen one's padawan, was a great duelist and acrobat, and is fulcrum!
What is it... a wart with a rock hat? - Charmedyeti
One of the podracers who was killed in Episode 1. In one of the deleted scenes it showed his family was there at the race before he got killed. So technically his family was there the whole event.
Sure why not? That's not dark at all. Why not have your family be at your execution while you're at it.
Huh? Why? I mean I get the movies could have happened without him, and frankly I didn't like him that much, but really?
What he is awesome
If you look at the top it says 0% voted for him
This person is trying to tick us off - CharmedyetiV 2 Comments
Um excuse me but he had a lot to do the story line
What the hell? Vader is the greatest Star Wars character! Without him, Star Wars would have become nowhere near as successful as it is now. - Goku02
In all 6 movies and his presence is strongly felt in episode 7
Can someone find out who put him on gere so I can murder he/she - CharmedyetiV 8 Comments
Excuse me! The whole original trilogy was based around him. How could he be pointless? Without him, Darth Vader would have never been redeemed.
Whoever put Luke on this list is the worst user on TheTopTens. - TopTenJackson
He shouldn't be here
Again, someone murder this person - CharmedyetiV 5 Comments
Recommended Lists
Related ListsTop Ten Star Wars Characters Favorite Star Wars Characters Top Ten Star Wars Prequel Trilogy Characters Top Ten Greatest Star Wars Characters Top Ten Original Trilogy Star Wars Characters
List StatsUpdated 26 Jul 2017
100 listings
7 years, 340 days old
Top Remixes (10)
2. Darth Maul
3. Boss Nass
2. Darth Maul
3. General Grievous
View All 10


text:
Find best Tuition in Punkunnu, Thrissur
Post your
Get custom responses
with in few hours
Compare & hire
the best one
Select from 16 Tuition near you
Find Now
UrbanPro in the News
UrbanPro provided me a platform to reach out to customers who eventually take up my course...
- Taha Zaidi
UrbanPro.com is a great platform to connect Professionals with customers who require right kind of guidance...
- Neera Mathur
UrbanPro is a wonderful platform for the Professionals to connect with customers and vice-versa...
- Sonu
UrbanPro is #1 Marketplace for finding Tutors & Classes
Students Helped
Punkunnu, Thrissur
2 Yrs experience
Classes: Tuition, SQL Programming and more.
I have completed MCA. I have done B, Sc in Statistics,
Punkunnu, Thrissur
5 Yrs experience
Classes: Tuition BTech Tuition
Being a B.Tech in Mechanical Engineering , I have been taking tuition for Engineering Graphics since 2012. The Graphics will be taught in an easy manner through...
Punkunnu, Thrissur
2 Yrs experience
Classes: Tuition, Class I-V Tuition
I have taught in a private school at palakkad for science, mathematics and english, worked in an engineering college as teaching assistant for two years.have taken...
Punkunnu, Thrissur
1 Yr experience
Classes: Tuition, Class XI-XII Tuition (PUC) and more.
Punkunnu, Thrissur
Classes: Tuition, Class I-V Tuition and more.
conducted many tuition for students
Punkunnu, Thrissur
1 Yr experience
Classes: Tuition, Class XI-XII Tuition (PUC)
I have been teaching for roughly a year. According to me one can achieve higher understanding of a subject by understanding the basic concepts. I teach Physics...
Punkunnu, Thrissur
8 Yrs experience
Classes: Tuition BTech Tuition
I am a graduate in Mechanical Engineering. My M Tech is in Technology Management. I have a total of 9 years teaching experience 5 years I worked as lecturer in SCMS...
Post your requirement and let us connect you with best possible matches for Tuition
Punkunnu, Thrissur
Classes: Tuition, Class I-V Tuition and more.
I can teach each and every topics very easily and make it stronger for the students.
Punkunnu, Thrissur
1 Yr experience
Classes: Tuition, BA Tuition and more.
After my post graduation in MBA HRM, I choose my profession as teaching.Currently I am employed with a business school where I am taking classes for mba hrm, bba,...
Punkunnu, Thrissur
12 Yrs experience
Classes: Tuition, Class IX-X Tuition
To make the student understand the topic and should use it as tool to shape his future
Punkunnu, Thrissur
20+ Yrs experience
Classes: Tuition Class XI-XII Tuition (PUC)
25 years of teaching at degree level 11years pg level 15 years helping students in Entrance classes
UrbanPro.com helps you connect with the best Tuition in Punkunnu,Thrissur, Kerala. Post Your Requirement today and get connected.


text:
Deals are valid from LA or San Francisco. If that's not home, FareCompare can get you there, cheap.
Sample Air New Zealand fares, round-trip prices:
From Los Angeles or San Francisco
Book deals to New Zealand by Nov. 25, book deals to Australia by Dec. 3. Travel dates vary but include winter, spring and summer. See Air New Zealand for all the details. See FareCompare for more cheap flights anywhere.
LISTEN: Fuel prices are down. Will airfares follow?


text:
February 11, 2010 at 01:25:51 Feb 11, 2010 @ 01:25
gonna check out the wesc's myself..
wesc... no...
edit: 22" thighs can fit into NC?? Sized down?? dayam... I thought nc were the skinny fit
aren't APC PS good for ppl w/ big thighs?
Hey Im 193lbs 5'10 with a 24 inch thigh, and and 34 inch waist. Im ordering some NS this week and I dont know if I should get a 33 or a 32.I want a 514 type of fit. Any help? This thread is what Ive been waiting for &) I
are imperial dukes good for guys with big thigh?
I am 5'10" 193lbs with 24" thighs and 34 waist. I got sz 33 NS, there should be a fit pic in this thread several posts back.
Cuban, that fit is really good. I shoulda gotten PS but the store didn't have my size The crotch will stretch out and get lap creases in no time and it will look real good I bet.


text:
Neither of those guys approached you with an inappropriate salacious come on. One guy was maybe a little forward and the other was clearly making a joke – ie flirting. So, if those men are the options cited for supposedly "looking for sex" on your other site, I think you may have more options than you think.-DMN
Personally, I don't think those comments were particularly rude. But, it's really a separate issue. The issue as originally framed here is that these comments are rude yes but also that they make us feel bad because they reflect a focus on our bodies and not our minds or characters. I just don't see a distinction between that and lusting publicly after a guy at the gym because you like his ass. I just can't imagine the critique of a male blogger who publicly wrote this stuff about his gym crush. Lacks principle. That's all. Carry on.- DMN
Okay. Let's unpack these two comments. Starting with:
Neither of those guys approached you with an inappropriate salacious come on. (For context see the texts below.)


text:
Apple macbook pro 13 inch Key Features:
- Mac OS X Lion
- Intel Core i7 3rd Gen
- 13.3 inches Screen
- 1280 x 800 pixels
- 750GB SATA Hard Disk
- up to 7 hours Battery Backup
- View all Specs »
- Apple has made available Apple macbook pro 13 inch in India.
- This laptop has Mac OS X Lion Operating System and Intel Core i7 3rd Gen Processor which is supported by 8GB DDR3 RAM.
- The Screen size is 13.3 inches and screen resolution is 1280 x 800 pixels.
- The laptop has 750GB SATA Hard Disk.
- It has Intel HD 4000 Graphics processor.
- Connectivity options in the laptop include USB, Wi-Fi, Bluetooth, RJ45LAN and HDMI.
- This laptop offers up to 7 hours Battery backup.


text: Images from The Legendary Starfy. Boxart American boxart.Japanese boxart.Add a photo to this galleryArtwork StarfyStarfy, again!Starfy using his Star SpinStarfy means business!MonstarStarpedoRoostarStarfrightStarlyStarfy and StarlyMoeBunstonMermaidOld Man LobberSnipsRonkPapesThe Terrible TrioAdd a photo to this galleryScreenshots CutsceneAdd a photo to this gallery Retrieved from "http://nintendo.wikia.com/wiki/The_Legendary_Starfy_(video_game)/gallery?oldid=287213" Ad blocker interference detected! Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers Wikia is not accessible if you've made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected. Categories: Galleries


text:
We can magically reduce tooth decay with fluoride treatments during your routine exam.
While fluoride treatments can help adults, they are especially important for children between the ages of 6 months and 16 years. This is because children begin losing their baby teeth and start to develop their permanent teeth.
- Strengthen enamel
- Remineralize the teeth and reverse potential tooth decay occurrence
It can also help adults who are suffering from dry mouth, gum disease, or frequent cavities. Fluoride treatments are quick and easy to receive and can drastically help the state of your smile.


text:
Bust of Piet Heyn, Hendrik de Keyser (II) (attributed to), 1636
Piet Heyn became a seaman at a young age. When he was fifteen years old, he was taken prisoner by the Spanish and made to serve two years as a galley slave. After his release, Heyn pursued a career in the merchant marine: he held high-ranking positions in the Dutch West India Company. In 1628 he captured a Spanish treasure fleet (known as the 'Silver Fleet') off the coast of Cuba. A year later he perished at sea.


text:
I am here but where do I start?
This will just be very random. :)
First: School
I still LOVE, LOVE, LOVE My Father's World. We are not as far along as I would like to be. Since starting school the kids took a vacation with my parents to St. Augustine. (I really want to go next time.) They LOVED it! Then we had three or four different revivals, then we took a vacation.....so, I am trying to settle down before the holidays and pick up the pace.
I am so pleased with how Jenna is progressing with her reading. Just out of curiosity I gave her a Bob Book She read it so well and was so excited. She is in week 7 of My Father's World K.
We had a homeschool History event. My crew was Jane Austen, Wyatt Earp, Maid Marian.
Thanks to my Mom, who is so sweet to always make whatever they come up with on a somewhat short notice. She made the girls dresses. She made one for Janie too, just like Jenna's, but the little sweetheart refused to wear it!
Vacation: The Sunday afternoon before my husbands "stay-cation" was to start he said "Let's go to the mountains!" and so just like that 12 hours later we were all packed up and on our way to the Great Smoky Mountains. It is our favorite vacation spot!
Birthdays: Josh turned 11. Janie turned 2 and Dad turned.....uh.....should I say it? 41. :P
|She was caught licking the spoon! :)
Autumn: My absolute favorite time of year. We had a Fall Fellowship at church. We did a Trunk or Treat and encouraged the kids to dress as bible characters. Here we have my two: Queen Esther and her maid. :)
This was the first time I have ever seen a Trunk or Treat. Here are some pics of the trunks. My idea was taken from a Google search, but since I am the pianist I thought it appropriate to
do a song. "Tis So Sweet To Trust in Jesus."
|Daniel in the den of lions.:) and the Empty Tomb
|Jonah and the Whale
|Another version of the empty tomb.
So, lets see, what else. Well, I have ran out of time and thoughts. I am ready for rest and a regular routine. I'll leave you with a picture of what I think is a perfect glimpse of the little things that reminds me to count my blessings.
|Looking through my door as the sun streams through the trees on a crisp autumn morning. Bliss :)


text:
Every time my son comes home for a visit he requests this Chocolate Trifle. It is one of my many easy homemade dessert recipes that I am asked to make for all occasions. It's always a hit for any get together or party. Continue reading "Easy Homemade Dessert Recipes – Chocolate Trifle" »
Best Snow Ice Cream
Three simple ingredients is all you need to make the absolute best snow ice cream. Oh my goodness, it's delicious. Every time it snows I make this easy treat for my family. They just love it and it's so much fun to make.
NFL Playoff Party Food – Sweet n Sour Meatballs
Who's going to the Superbowl? That is the million dollar question. These sweet n sour meatballs are a huge hit when it comes to NFL playoff party food ideas. They will stay warm in a crock pot and you can pop them in your mouth all day long. Don't forget your favorite beer to go […]
Tailgating Recipes – Twisted Chicken Wings
This is an oldie but a goodie when it comes to tailgating recipes because who doesn't love chicken wings to munch on when they are watching football? My twisted chicken wings are even better the next day. Make them Saturday and munch all day on Sunday.
Easy Tailgating Recipes – Old Bay Wings
Are you ready for some football? Whether you are looking for easy football food recipes or an easy tailgating recipe this is a winner! Here in Maryland Old Bay is a staple in our kitchen and chicken wings are a must during a game. These wings are a football snack hit, especially with my blue […]
Best Ever Taco Cups is an Easy Tailgating Recipe
My family simply loves it when I make this best ever taco cups recipe for game day. This is an easy finger food snack recipe for football that nobody can turn down. So yummy I figured they were worth reposting. Don't forget these are also an easy tailgating recipe, too.
Easy Homemade Dessert Recipes – Chocolate Trifle
Balance Bare Nutrition Energy Bars
It's the week after Thanksgiving and I ate a lot. Who didn't, right? In my never-ending quest to stay fit and not blow up like a cow I am heading back to the gym. The only thing is, after working 8 hours at my day job I really don't have the energy to go. I needed that extra boost around 3:30 in the afternoon and I found the perfect, most delicious energy bars. I find that eating 1 Balance Bare Nutrition Energy Bar along with a piece of fruit gives me the boost I need. They are amazing and come in different flavors. Get the energy you need and keep fit while not sacrificing a thing.
Best Pumpkin Cupcake Recipe
Sometimes you are just too full after a big Thanksgiving meal to eat slices of pumpkin pie and pumpkin roll. I've come up with the best pumpkin cupcake recipe that will satisfy your sweet tooth but not send the button flying off your blue jeans. It is the perfect amount of dessert. Continue reading "Best Pumpkin Cupcake Recipe" »
Leftover Thanksgiving Turkey Soup
Leftover Thanksgiving Turkey Soup is a great way to use up all that turkey. With this Polar Vortex we have been experiencing a nice hot soup will warm everyone's bones. Take some of those leftover rolls and dip it right in the broth. Continue reading "Leftover Thanksgiving Turkey Soup" »
Leftover Thanksgiving Turkey Pot Pie
No one really feels like cooking after Thanksgiving but you always have so much turkey to get eaten up. My Leftover Thanksgiving Turkey Pot Pie takes about 15 minutes to throw together and it's so good. I love it and make it every year. Continue reading "Leftover Thanksgiving Turkey Pot Pie" »
Tailgating Recipes – Southwest Salsa
I don't go to football games for the football, I go for all the great tailgating food. My Southwest Salsa is a great tailgating recipe. The taste of freshness in the middle of the winter is awesome. Continue reading "Tailgating Recipes – Southwest Salsa" »
Recipe for Venison Sausage Balls
This Recipe for Venison Sausage Balls is great for tailgating or football parties. They're a great finger food you can pop right in your mouth. Continue reading "Recipe for Venison Sausage Balls" »
Recipe for Easy Chili Mac
My recipe for Easy Chili Mac is done right on your stove top. One of those one pot wonders. Sometimes it seems the more simple my recipes are the more my family likes them. Continue reading "Recipe for Easy Chili Mac" »
Recipe for Spaghetti Squash
I adore pasta and all the fixings but my waistline and cholesterol aren't loving it so much anymore. This recipe for spaghetti squash is healthy yet so very tasty. You would never realize you aren't eating pasta. Hey, what they don't know won't hurt them, right? Continue reading "Recipe for Spaghetti Squash" »


text:
Kingsmen Challenge Royals
CLU falls to HIU 3-1
FULLERTON, Calif. – The Cal Lutheran men's volleyball team took on Hope International on Tuesday evening and battled the Royals before falling 3-1 (25-17, 25-21, 23-25, 25-20) at Darling Pavilion.
In the first set, HIU used a strong .471 hitting percentage with just one error to take the set 25-17 after jumping out to an early lead. In the second, the Kingsmen trailed 7-5 early before an 8-3 spurt from the Royals helped them pull away and take a 2-0 set lead.
CLU rallied in the third set for a narrow 25-23 victory to stay alive. Back-to-back kills from Patrick Rowe and Mason Mercer opened the scoring for the Violet and Gold, who later found themselves tied with HIU at 20-20. Down the stretch, Michael Campbell came up with a pair of critical kills, including the game-winner.
Despite hitting .393 as a team in the fourth set, the Kingsmen fell behind early to the Royals and dropped the set 25-20.
Rowe tied for game-high honors with 17 kills while adding 14 digs for a monster double-double. Mercer set a new career-high with 14 kills and Mikey Esper finished with eight. Nick Shoemate also tallied a career-high with 49 assists while Jamal Balkhi notched double-figures with 11 digs.
The Royals were led by 17 kills apiece from Zach Greene and Kevin Baran-Maguire.
Cal Lutheran (5-15) returns home for its next match against Concordia-Irvine on Wednesday, Mar. 29 at 7:00 p.m. inside Gilbert Arena.
Box Score: HIU 3, CLU 1
Tournament Central: Second Annual Cal Lu Fornia Invitational
CLU Instagram: http://instagram.com/clusports#
M Volleyball Instagram: https://instagram.com/kingsmen_volleyball/
CLU Twitter: https://twitter.com/clusports
M Volleyball Twitter: https://twitter.com/CLUmVolleyball
CLU Facebook: https://www.facebook.com/clusports


text:
A maths teacher, Oksana Neveselaya has become a web sensation for her sexy selfies after a class of her teaching maths was posted on YouTube by a student. The 15-second footage quickly went viral and beautiful Oksana has since amassed thousands of followers on social media.
Miss Neveselaya, from Minsk, Belarus, has since swept YouTube and garnered a huge Instagram following of more than 173,000 devoted fans.


text: There are two basic versions of this Austrian dumpling. The heartier, flour-based, savory rendition is served in soups and stews. The sweet version, known as Salzburger nokerl contains very little flour and is made fluffy by the addition of stiffly beaten egg whites. It's generally used as an addition to fruit soups or served for dessert accompanied by fruit.