Abstract
This entry provides reusable theories that lift properties of first-order (ground and nonground) terms to atoms, literals, and clauses. These properties include substitutions, orders, entailment, and typing. The sessions AFP/First_Order_Terms and AFP/Abstract_Substitution are the basis of this entry.
License
Topics
Session First_Order_Clause
- Context_Notation
- Typing
- Term_Typing
- Generic_Context
- Parallel_Induct
- IsaFoR_Ground_Term
- IsaFoR_Ground_Context
- Ground_Term_Typing
- Nonground_Term
- Multiset_Extra
- Multiset_Grounding_Lifting
- Nonground_Clause_Generic
- Selection_Function
- Nonground_Selection_Function
- HOL_Extra
- Grounded_Selection_Function
- IsaFoR_Nonground_Term
- Literal_Functor
- Uprod_Extra
- Uprod_Literal_Functor
- Nonground_Clause_With_Equality
- IsaFoR_Nonground_Clause_With_Equality
- Nonground_Context
- Context_Functor
- IsaFoR_Nonground_Context
- Restricted_Order
- Context_Compatible_Order
- Term_Order_Notation
- Transitive_Closure_Extra
- Ground_Term_Order
- Grounded_Order
- Nonground_Term_Order
- Multiset_Extension
- Natural_Functor_To_Multiset
- Grounded_Multiset_Extension
- Maximal_Literal
- Term_Order_Lifting
- Ground_Order_Generic
- Nonground_Order_Generic
- Ground_Order_With_Equality
- Nonground_Order_With_Equality
- Selection_Function_Select_Max
- IsaFoR_KBO
- Nonground_Clause
- IsaFoR_Nonground_Clause
- Ground_Term_Rewrite_System
- Ground_Critical_Pairs
- Ground_Critical_Peaks
- IsaFoR_Ground_Critical_Pairs
- Collect_Extra
- Infinite_Variables_Per_Type
- Typed_Functional_Substitution
- Nonground_Term_Typing
- Monomorphic_Typing
- Entailment_Lifting
- Fold_Extra
- Nonground_Entailment
- Inference_Functor
- Nonground_Inference
- Ground_Order
- Nonground_Order
- Natural_Magma_Typing_Lifting
- Multiset_Typing_Lifting
- Clause_Typing_Generic
- Typed_Functional_Substitution_Lifting
- Nonground_Typing_Generic
- Clause_Typing
- Nonground_Typing
- Clause_Typing_With_Equality
- Nonground_Typing_With_Equality
- Typed_Functional_Substitution_Example
- Typed_Functional_Substitution_Lifting_Example
- Tiebreakers
- Typed_Tiebreakers
- Untyped_Calculus
Depends on
- Abstract Substitution
- First-Order Terms
- Fresh identifiers
- Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering
- Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
- Regular Sets and Expressions
- Regular Tree Relations
- Extensions to the Comprehensive Framework for Saturation Theorem Proving
- A Generic Framework for Verified Compilers