Atom

An Atom is simply a GeneralizedAtom using SkolemTerms.

@[reducible, inline]

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

Equations

• Atom sig = GeneralizedAtom sig (SkolemTerm sig)

def FunctionFreeAtom.skolemize {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : Rule sig) (i : Nat) (lt : i < rule.head.length) (a : FunctionFreeAtom sig) : Atom sig

We can skolemize a FunctionFreeAtom by skolemizing all its VarOrConsts. This yields an Atom.

Equations

• FunctionFreeAtom.skolemize rule i lt a = { predicate := a.predicate, terms := List.map (VarOrConst.skolemize rule i lt) a.terms, arity_ok := ⋯ }

@[simp]

theorem FunctionFreeAtom.length_skolemize {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : Rule sig} {i : Nat} {lt : i < rule.head.length} {a : FunctionFreeAtom sig} : (skolemize rule i lt a).terms.length = a.terms.length

The number of terms remains unchanged when Skolemizing.

theorem FunctionFreeAtom.mem_skolemize_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : Rule sig} {i : Nat} {lt : i < rule.head.length} {a : FunctionFreeAtom sig} {t : VarOrConst sig} : t ∈ a.terms → VarOrConst.skolemize rule i lt t ∈ (skolemize rule i lt a).terms

If a a VarOrConst occurs in the terms of the FunctionFreeAtom, then the Skolemized VarOrConst occurs in the Skolemized Atom.