dfs_logic.pl -- First-order Logic

This module implements basic first-order logic operations and properties on formulas and vectors.

 dfs_conjoin(+FormulaSet, -Conjunction) is det

True if Conjunction is a logical conjunction of the formulas in FormulaSet.

 dfs_disjoin(+FormulaSet, -Disjunction) is det

True if Disjunction is a logical disjunction of the formulas in FormulaSet.

 dfs_complement(+Formula, +ComplementFormula) is det

ComplementFormula specifies the falsehood conditions of Formula.

 dfs_conj_vector(+Vector1, +Vector2, -ConjVector) is det

ConjVector is the conjunction (component-wise product) of Vector1 and Vector2.

 dfs_validity(+Formula, +ModelSet) is det

dfs_validity(+Formula, +ModelMatrix) is det

A formula P is valid (|= P) iff P is true (not false) in all models.

 dfs_satisfiability(+Formula, +ModelSet) is det

dfs_satisfiability(+Formula, +ModelMatrix) is det

A formula P is satisfiable iff P is true in at least one model M.

 dfs_entailment(+FormulaP, +FormulaQ, +ModelSet) is det

dfs_entailment(+FormulaP, +FormulaQ, +ModelMatrix) is det

A formula P entails a formula Q (P |= Q) iff Q is true in every model that satisfies P.

 dfs_logical_equivalence(+FormulaP, +FormulaQ, +ModelSet) is det

dfs_logical_equivalence(+FormulaP, +FormulaQ, +ModelMatrix) is det

A formula P is logically equivalent to formula Q iff [[P]]^M,g = [[Q]]^M,g for all models M and variable assignments g