First-Order Logic and Horn Clauses

A set of flashcards covering key concepts and terms related to First-Order Logic, Horn Clauses, and logical reasoning methods.

First-Order Logic (FOL)

A formal logical system that allows quantification over objects and the use of predicates.

Horn Clause

A logical formula that is a disjunction of literals, where at most one literal is positive.

Forward Chaining

A reasoning method that starts with known facts and applies rules to infer new facts.

Backward Chaining

A reasoning method that starts with a goal and works backward to see if known facts support it.

Generalized Modus Ponens (GMP)

A logical rule that allows inferring new facts from existing ones based on Horn clauses.

Positive Horn Clause

A Horn clause containing only positive literals, with no negations.

Negative Horn Clause

A Horn clause consisting solely of negative literals, where all literals are negated.

Mixed Horn Clause

A Horn clause that includes at most one positive literal, with the rest being negative.

Skolemization

The process used to eliminate existential quantifiers from logical formulas.

Conjunctive Normal Form (CNF)

A way of structuring a logical formula as a conjunction of disjunctions.

Implication

A logical connective typically represented as P → Q, which can be rewritten as ¬P ∨ Q.

De Morgan's Laws

Rules for transforming logical expressions involving negation, including ¬(P ∨ Q) = ¬P ∧ ¬Q.

Predicate

A function or relation that can be true or false depending on the values of its variables.

Quantifier

An operator that specifies the quantity of specimens in the domain of discourse that satisfy an open formula.

Universal Quantifier (∀)

Indicates that a statement applies to all elements in a given domain.

Existential Quantifier (∃)

Indicates that there exists at least one element in a given domain that satisfies a statement.