Typed Ordered Resolution (Q7361289)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Typed_Ordered_Resolution
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Typed Ordered Resolution |
AFP entry Typed_Ordered_Resolution |
Statements
11 June 2025
0 references
Adnan Mohammed Ahmed
0 references
Balazs Toth
0 references
Typed Ordered Resolution (English)
0 references
Ordered Resolution is a proof calculus for reasoning about first-order logic that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this formalization, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects. We also added a type system to the calculus. We relied on the library for first-order clauses and on the saturation framework.
0 references
