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
- Ground_Term_Extra
- Ground_Context
- Multiset_Extra
- Uprod_Extra
- Ground_Clause
- Typing
- Natural_Magma_Typing_Lifting
- Multiset_Typing_Lifting
- Clausal_Calculus_Extra
- Clause_Typing
- Context_Extra
- Term_Typing
- Ground_Typing
- Nonground_Term
- Nonground_Context
- Multiset_Grounding_Lifting
- Nonground_Clause
- Selection_Function
- Nonground_Selection_Function
- Infinite_Variables_Per_Type
- Collect_Extra
- Typed_Functional_Substitution
- Functional_Substitution_Typing
- Typed_Functional_Substitution_Lifting
- Functional_Substitution_Typing_Lifting
- Nonground_Term_Typing
- Nonground_Typing
- HOL_Extra
- Grounded_Selection_Function
- Term_Rewrite_System
- Entailment_Lifting
- Fold_Extra
- Nonground_Entailment
- Nonground_Inference
- Restricted_Order
- Context_Compatible_Order
- Term_Order_Notation
- Transitive_Closure_Extra
- Ground_Term_Order
- Grounded_Order
- Multiset_Extension
- Grounded_Multiset_Extension
- Maximal_Literal
- Term_Order_Lifting
- Ground_Order
- Nonground_Term_Order
- Nonground_Order
- Typed_Functional_Substitution_Example
- Typed_Functional_Substitution_Lifting_Example
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