# Knowledge Engineering

Knowledge engineering is the process of figuring out how to represent propositions and logic in AI. Humans reason based on existing knowledge and draw conclusions, and we want to be able to recreate that in AI.

This is directly linked to what I learned in MATH135.

**Knowledge-Based Agents**
These are agents that reason by operating on internal representations of knowledge.

### Propositional Logic

Propositional logic is based on propositions, statements about the world that can be either true or false.

**Sentence**
A sentence is an assertion about the world in a knowledge representation language. A sentence is how AI stores knowledge and uses it to infer new information.

**Knowledge Base (KB)**
The knowledge base is a set of sentences known by a knowledge-based agent. Given in the form of propositional logic sentences that can be used to make additional inferences about the world.

**Entailment (âŠ¨)**
If Î± âŠ¨ Î˛ (Î± entails Î˛), then in any world where Î± is true, Î˛ is true, too.

For example, if Î±: â€śIt is a Tuesday in Januaryâ€ť and Î˛: â€śIt is a Tuesday,â€ť then we know that Î± âŠ¨ Î˛. If it is true that it it a Tuesday in January, we also know that it is a Tuesday.

### Inference

Inference is the process of deriving new sentences from old ones.

There are several models we can use. Model Checking Algorithm

### Inference Rules

These are basic rules, they include rules about

- Implication
- De Morganâ€™s Laws (DML)
- Double Negation
- If and Only If
- [[notes/De Morganâ€™s Laws (DML)#Distributive Laws|De Morganâ€™s Laws (DML)#Distributive Laws]]

### Knowledge and Search Problems

Inference can be viewed as a search problem with the following properties:

- Initial state: starting knowledge base
- Actions: inference rules
- Transition model: new knowledge base after inference
- Goal test: checking whether the statement that we are trying to prove is in the KB
- Path cost function: the number of steps in the proof

### Resolution

Resolution is a powerful inference rule that states that if one of two atomic propositions in an Or proposition is false, the other has to be true. For example, given the proposition â€śRon is in the Great Hallâ€ť Or â€śHermione is in the libraryâ€ť, in addition to the proposition â€śRon is not in the Great Hall,â€ť we can conclude that â€śHermione is in the library.â€ť More formally, we can define resolution the following way: