Facts

A Fact is a GeneralizedAtom with GroundTerms.

@[reducible, inline]

abbrev Fact (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max (max u_3 u_2) u_1) u_1)

Equations

• Fact sig = GeneralizedAtom sig (GroundTerm sig)

def Fact.constants {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) : List sig.C

The Fact.constants are the constants of all terms.

Equations

• f.constants = List.flatMap GroundTerm.constants f.terms

def Fact.function_symbols {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) : List (SkolemFS sig)

The Fact.function_symbols are the function symbols of all terms.

Equations

• f.function_symbols = List.flatMap GroundTerm.functions f.terms

def Fact.isFunctionFree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (f : Fact sig) : Prop

A Fact is function free, if each term is a constant.

Equations

• f.isFunctionFree = ∀ (t : GroundTerm sig), t ∈ f.terms → ∃ (c : sig.C), t = GroundTerm.const c