A logic machine can add new sentences to a knowledge base using the rules of inferences. A logic machine can have the algorithm to do so.
When a sentence α is added to the knowledge base by a logic machine using the rules of inferences then we can say that,
α is provable.
KB ├─ α
A proof system is defined by two things: premises (or axioms) and rules of inference. To proof a sentence truthiness, we use those premises and rules to synthesis new sentences and in the end the sentence we want to prove.
There are two types of proofs:
- Direct proofs. It goes from given premises to proof the conclusion.
- Indirect proofs