Clausal Form in AI
First-order logic is subdivided into clausal forms. In this standard form, a matrix and a universal prefix describe a sentence. The formula is expressed in clausal form as a series of clauses, each of which consists of a number of literals joined by just OR logical connectives.
Propositional resolution is limited to clausal expressions. Thankfully, any set of propositional calculus statements may be converted into an equivalent set of phrases in clausal form.
The following quantifiers are possible in a formula:
Universal Quantifier
The statement "For all x, P(x) holds" can be used to interpret it, indicating that P(x) holds true for all x in the universe.
For example: All BUS are wheeled.
Existential Quantifier
"There exists an x such that P(x)" indicates that P(x) is true for at least one universely object, x.
For example: You are loved by someone.
Properties of AI's Clausal Form
A formula in clausal form needs to be changed to one that has the following properties:
1. Every variable in the equation has a universal quantification. Therefore, it's not required to explicitly include the universal quantifiers for everyone. The universal quantifier implicitly quantifies each variable in the formula after the quantifiers are eliminated.
2. The formula consists of many clauses, each of which is made up of multiple literals joined by logical connectives called OR. Every clause is therefore a disjunction of literals.
3. The only logical connectives used to join the sentences together to build a formula are AND. A conjunction of clauses is hence a formula's clausal form.
Example of Clausal Form in AI
Positive and negative literals are two types of literals. Regarding the separate clause forms, where each one is a literal disjunction. Regarding the form of the clause:
Consider the following example:
"We know that all Romans who know Marcus either think that anyone who hates anyone is crazy or they hate Roman."
As shown in the properly structured formula (the wff):
∀x: [Know(x, Marcus) ^ Roman(x)] ⇒ [think crazy(x, y)) → hate(x, Caesar) V (∀y : (̎z : hate(y, z))]
