Logic Concepts in FCPL and CFOL

Introduction to Symbolic Artificial Intelligence

• Course: INF4067
• Semester: S8 - MAJ
• Academic Year: 2024-2025
• Subject matter: Predicate Logic

Section Outline

• Full Classical First-Order Logic (FCFOL): A relational extension of FCPL.
• Horn Classical First-Order Horn Logic (HCFOL): A practical trade-off between expressiveness, explainability, and inference scalability.

Section Readings

• First-Order logic: AIMA4 chapters 8 and 9

KRL Properties: Procedural vs. Declarative

• Procedural: Knowledge is structured into application-specific data and functions. Manual programming is required for each application.
• Declarative: Application-specific sentences are used. Application-independent inference engines (IEs) are used to infer new sentences. Knowledge bases only contain relations between properties.

KRL Properties: Compositionality, Structure, and Relation

• Compositional: Complex sentences are built from atomic sentences.
• Structured: Atomic sentences describe properties over complex data structures.
• Relational: A universal relation between all individuals from given classes can be expressed concisely in a single sentence.

Full Classical First-Order Logic (FCFOL)

• Diagram describes the structure of FCFOL, including composite, connected, binary, and unary FCFOL.
• Includes sub-components like quantifier expressions, logical variables, ground terms, leaf terms, atomic formulas, etc.
• Examples are shown of different possible expressions.

FCFOL vs FCPL as WW Agent KRL

• FCFOL representations are more concise and faster.
• Manual specification is simpler in FCFOL.
• The video notes conventions of logic in programming.

KR with FCFOL

• Ground terms: Represent individuals in an application domain.
• Constant terms: Represent values of unstructured properties.
• Logical Variables: Represent properties of concepts and individuals.
• Non-ground terms: Represent application concepts.
• Unary predicates: Represent Boolean properties.

FCFOL Semantic Models

• Atomic FCPL formulas merely connect unstructured symbols logically.
• Semantics come from cognitive association between symbols, IA's environment properties, and the knowledge engineer's input.

FCFOL Semantic Models

• FCFOL has a richer ontology, with four semantically distinct symbol types.
• Constants represent unstructured objects.
• Variables represent sets of unstructured objects.

FCFOL Semantic Example

• Examples from AIMA4 are used.
• Variables and functions are shown.

FCFOL Denotational Semantic Models

• Explains how to calculate a Herbrand model for FCFOL formulas.
• Shows steps in how to substitute and propositionalize.

Example of Herbrand Universe, Base and Model

• Example using Herbrand Universe, base, and the model calculation.
• Equivalent FCPL clauses are shown for the cases.

FCFOL Inference by Propositionalization

• FCFOL inference is reduced to evaluating FCPL inference.
• Propositionalization of formulas is a key step.

Herbrand's and Gödel's Theorems

• Herbrand's Theorem states that for an unsatisfiable set of clauses, a smaller finite subset is also unsatisfiable.
• FCFOL entailment is semi-decidable; there is no algorithm to guarantee a proof.

FOLAF Unification

• Unification is an extended equality in FOLAF.
• An algorithm is provided for FOLAF unification and an example of unification in use.

FOLAF Unification Algorithm

• The FOLAF unification algorithm proceeds recursively to unify terms.
• It checks for variable occurrences and function calls.

FOLAF Unification Example

• Example illustrating how the algorithm unifies FOLAF terms to find a substitution.

FCFOL Normal Forms

• Any FCFOLF can be manipulated to generate a normalized form.
• All quantifiers are moved to the left, for semantic purposes.
• Existentially quantified variables can be skolemized.

FOL Normal Forms

• Many sorted FOL (MSFFOL) extends FCFOL with sorts (types) to atomic formula predicate arguments restricting interpretation domain.
• Predicate arguments are restricted by sorts.

Horn CFOL (HCFOL)

• HCFOL: Horn restriction of FCFOL.
• Unification lifts clause chaining (forward and backward).
• Inference rule is sound and complete.

Horn FOL as a Specialization of FOL

• MSFFOL (many sorted full FOL): Extensions of FCFOL with sorts.
• Examples of implications and inferences are shown.
• Simplification when quantifiers, premises, and conclusions are all related.

HCFOL Forward Chaining Example

• Shows clauses related to a certain problem.
• Steps in chaining are displayed for reference.

HCFOL Backward Chaining

• Backward chaining the unification-based resolution inference rule is sound.
• It may be incomplete.
• Infinite loops cause problems during a depth-first search, like it is shown in the examples.

HCFOL Backward Chaining Example

• Shows the formalization and the chain to follow.

Non-Horn FCFOLF Resolution Example

• Example for non-Horn clauses.
• Some related inferences and substitutions are shown to arrive at the required conclusion.
• Resolution strategies are shown.

Resolution Strategies

• Key decisions in resolution-based Inference Engines (IEs) relate to resolutions' choice.
• Popular choices like unit preference, set of support, linear resolution, and selective linear definite (SLD) are shown.

Limitations of FCFOL

• No quantification over predicate names; high-order relations can't be directly represented.
• Monotonic reasoning means truth values don't change over time.

Example of Axiomatization and Reification

• The Event Calculus (EC) axiomatizes non-monotonic reasoning.
• Implementing non-monotonic state changes (via truth value updates) in a monotonic IE is possible using reification.
• Examples of specific predicates like 'happens', 'initiates', and 'terminates' are provided.

Four Top-Level Classes of IA Inferences

• Deduction: Derives new knowledge from existing knowledge and rules.
• Abduction: Infers possible causes from observed effects.
• Induction: Discovers general rules from specific observations.
• Analogy: Infers new knowledge based on similarity between situations.

FOL Inference Methods: Deduction

• From specific knowledge and general rules, derive specific knowledge.
• Inference engines like SAT solvers and theorem provers are involved in this inference.

FOL Inference Methods: Abduction

• Abduction infers possible causes from observed effects.
• C(a) is a possible cause for o(a).
• Inference engines based on Prolog or constraint logic programming are often used.

FOL Inference Methods: Induction

• Inducing general rules from specific observations.
• Validated by new observations.
• Decision trees and machine learning tools are often employed (e.g., ML ILP engines).

FOL Inference Methods: Analogy

• Inference based on similarity between situations.
• It uses similar knowledge in other fields through analogies.
• Instance-based reasoning and KNN algorithms are often used.

Inference Engine Diversity

• Different types of IEs are presented, with their pros and cons.
• There is mention of deductive search, non-monotonic reasoning, probabilistic reasoning, etc.

KRL Diversity

• Different knowledge representation languages (KRLs) are shown, with various characteristics and uses.
• Tree-based, graph-based, and sub-symbolic KRLs are noted.

This quiz explores key concepts in first-order logic and predicate calculus, focusing on predicates, quantifiers, and logical connectives. It also delves into the nuances of axiomatization and inference methods. Test your understanding of these foundational topics in logical reasoning.