Logic

We define formally:

• Logical entailment: sentences $P_1,P_2,\cdots ,P_n$ entail a sentence $P$ iff the truth of $P$ is implicit in the truth of $P_1,P_2,\cdots ,P_n$. That is, in any world where $P_1,P_2,\cdots ,P_n$ are true, then $P$ is also true.
• Logical inference is the process of calculating entailments.

Then, logic is defined as the study of entailment relations, truth conditions, and the rules of inference. We express logic with logical languages:

• They are mathematically precise, so we can analyse their limitations, properties, and the complexity of inferences.
• They’re formal languages, so computer programs can manipulate sentences in the language.
• And typically they have well-developed proof theories: formal procedures for reasoning to produce new sentences.

Categories

• First-order logic (FOL) is a type of logical language. It is the most expressive language that has a somewhat “appropriate” automated inference procedure, called resolution.
• Propositional logic only takes true or false as values.

Decidability

There is no procedure that can return true if a given set of clauses are unsatisfiable (or false if not). This is because resolution is refutation complete. If a set of clauses is unsatisfiable, and so some branch contains $()$, then a BFS is guaranteed to find $()$.

But search may not terminate on satisfiable clauses when the answer is NO.

In general:

• First-order unsatisfiability is semi-decidable, but not decidable.
• First-order satisfiability is undecidable.

Sub-pages

• Logic gate
• Knowledge representation and reasoning