Resolution Ontology

FLOW_ALGEBRA ResolutionOntology v1.0
TARGET_URL := "https://kirethresearch.org/booksai-core/ontologies/mathematical-ontologies/mathematical-logic-ontologies/logical-reasoning/resolution-ontology-2.html"
LANGUAGE := "en-GB"
DOMAIN := MathematicalOntologies > MathematicalLogicOntologies > LogicalReasoning > ResolutionOntology

BEGIN_FLOW

ENTITY Resolution {
 TYPE := FormalInferenceRule
 DEFINITION := "A refutation-oriented inference rule deriving resolvents from clauses containing complementary literals, central to propositional and first-order automated reasoning."
}
ENTITY Clause { TYPE := DisjunctionOfLiterals }
ENTITY Literal { TYPE := AtomicFormulaOrNegatedAtomicFormula }
ENTITY Resolvent { TYPE := DerivedClause }

RELATIONSHIP Resolution --takes_input--> Clause
RELATIONSHIP Resolution --matches--> ComplementaryLiteral
RELATIONSHIP Resolution --produces--> Resolvent
RELATIONSHIP Resolution --supports--> Refutation
RELATIONSHIP Resolution --uses--> Unification

CLAUSE {
 C := L1 OR ... OR Ln
}
EMPTY_CLAUSE {
 SYMBOL := BOX
 MEANING := Contradiction
}
UNIT_CLAUSE {
 C := {L}
}
COMPLEMENTARY_LITERALS {
 P AND NOT(P)
}

PROPOSITIONAL_RESOLUTION {
 C1 := P OR A
 C2 := NOT(P) OR B
 RESOLVENT := A OR B
}
GENERAL_RESOLUTION {
 C1 := L OR Gamma
 C2 := NOT(L) OR Delta
 RESOLVENT := Gamma OR Delta
}
RESOLUTION_SOUNDNESS {
 C1 AND C2 entails Resolvent
}
TAUTOLOGICAL_RESOLVENT {
 IF resolvent contains L and NOT(L)
 THEN may_discard_under_standard_optimisation
}

FIRST_ORDER_RESOLUTION {
 C1 := L OR Gamma
 C2 := NOT(L') OR Delta
 FIND MGU theta SUCH_THAT Ltheta=L'theta
 OUTPUT := (Gamma OR Delta)theta
}
UNIFICATION {
 INPUT := TermsOrAtoms
 OUTPUT := Substitution theta
}
MOST_GENERAL_UNIFIER {
 ABBREVIATION := MGU
 PROPERTY := every_other_unifier_factors_through_MGU
}
OCCURS_CHECK {
 variable x MUST_NOT unify_with term_containing_x
 under standard finite first-order terms
}
STANDARDISE_APART {
 rename variables in separate clauses before resolution
}
FACTORING {
 unify duplicate/similar literals within clause
 to support first-order completeness
}

RESOLUTION_REFUTATION {
 TO prove Gamma entails Goal:
  ADD NOT(Goal)
  CLAUSIFY
  REPEATEDLY derive resolvents
  IF EMPTY_CLAUSE derived:
   RETURN refutation_success
}
REFUTATION_PRINCIPLE {
 Gamma entails Goal
 IFF Gamma UNION {NOT Goal} is unsatisfiable
 under classical semantics
}

CLAUSIFICATION {
 PIPELINE := {
  EliminateBiconditionals,
  EliminateImplications,
  MoveNegationsInward,
  StandardiseVariables,
  Skolemise,
  DropUniversalQuantifiers,
  ConvertToCNF,
  ExtractClauses
 }
}
SKOLEMISATION {
 PURPOSE := remove_existential_quantifiers
 INTRODUCE := SkolemConstantsOrFunctions
 PRESERVES := equisatisfiability
 WARNING := not_unrestricted_equivalence
}
CNF {
 FORM := conjunction_of_clauses
}
CLAUSE_SET {
 S := {C1,...,Cn}
}
RESOLUTION_CLOSURE {
 S plus all clauses derivable by resolution_and_factoring
}
UNSATISFIABILITY_BY_RESOLUTION {
 IF EMPTY_CLAUSE in resolution_closure
 THEN clause_set_unsatisfiable
}
PROPOSITIONAL_COMPLETENESS {
 resolution_refutation is complete_for_propositional_unsatisfiability
}
FIRST_ORDER_REFUTATION_COMPLETENESS {
 resolution_with_unification_and_factoring is refutation_complete
 under standard theorem conditions
}

SATURATION {
 add nonredundant resolvents until:
  EmptyClause OR NoNewClauses OR ResourceLimit
}
GIVEN_CLAUSE_ALGORITHM {
 PASSIVE := unprocessed_clauses
 ACTIVE := processed_clauses
 LOOP:
  select_given_clause
  simplify
  generate_inferences
  move_to_active
  enqueue_new_clauses
}
SET_OF_SUPPORT {
 restrict resolution so support ancestry participates
 REQUIRE completeness_conditions_if_claimed
}
UNIT_PREFERENCE {
 prefer unit_resolution
}
UNIT_RESOLUTION {
 P
 NOT(P) OR Q
 ----
 Q
}
INPUT_RESOLUTION {
 at_least_one_parent_is_input_clause
 WARNING := not_complete_for_arbitrary_clause_sets
}
LINEAR_RESOLUTION {
 each new resolvent uses previous resolvent as parent
}

SLD_RESOLUTION {
 TYPE := RestrictedLinearResolution
 USED_BY := LogicProgrammingAndHornClauses
 COMPONENTS := {SelectionRule,Unification,GoalReduction}
}
SLD_STEP {
 SELECT goal A_i
 SELECT clause H <- B1,...,Bk
 UNIFY A_i,H WITH theta
 NEW_GOAL := remaining_goals + body_goals under theta
}
SLD_REFUTATION {
 SUCCESS := EmptyGoal
}
HORN_CLAUSE {
 at_most_one_positive_literal
}
DEFINITE_CLAUSE {
 exactly_one_positive_literal
 LOGIC_PROGRAM_FORM := Head <- Body
}
PROLOG_RELATIONSHIP {
 Prolog commonly uses SLD-style_resolution + unification + ordered_search
}

HYPERRESOLUTION {
 TYPE := GeneralisedResolutionMethod
}
PARAMODULATION_RELATIONSHIP {
 equality_reasoning MAY require paramodulation
}
SUPERPOSITION {
 TYPE := ResolutionRelatedEqualityCalculus
 PURPOSE := theorem_proving_with_equality
}

SUBSUMPTION {
 C subsumes D IF some substitution theta makes Ctheta subset_of D
}
FORWARD_SUBSUMPTION {
 existing_clause_subsumes_new -> discard_new
}
BACKWARD_SUBSUMPTION {
 new_clause_subsumes_existing -> remove_existing
}
TAUTOLOGY_DELETION {
 remove tautological clauses
}
DUPLICATE_LITERAL_DELETION {
 P OR P OR Q -> P OR Q
}
CLAUSE_SIMPLIFICATION {
 METHODS := {
  TautologyDeletion,
  DuplicateLiteralDeletion,
  Subsumption,
  Rewriting,
  UnitSimplification
 }
}

RESOLUTION_TRACE {
 RECORD := {
  Step,
  ParentClause1,
  ParentClause2,
  ResolvedLiterals,
  Unifier,
  Resolvent,
  Simplifications
 }
}
VERIFY_RESOLUTION_STEP(S) {
 IDENTIFY parents
 IDENTIFY complementary_literals
 IF first_order:
  VERIFY unifier
 CONSTRUCT expected_resolvent
 APPLY declared_simplification
 COMPARE with recorded_resolvent
 RETURN valid_or_failure
}
VERIFY_RESOLUTION_PROOF(P) {
 FOR_EACH derived_clause:
  VERIFY_RESOLUTION_STEP
 RETURN valid_if_all_steps_valid
}

SEARCH_STRATEGY {
 SELECT clauses_and_literals
 to control combinatorial_explosion
}
CLAUSE_SELECTION {
 CRITERIA := {Age,Weight,LiteralCount,GoalRelevance,SymbolComplexity}
}
ORDERED_RESOLUTION {
 restrict eligible inferences using ordering
 REQUIRE completeness_conditions_if_claimed
}
REDUNDANCY_ELIMINATION {
 remove redundant clauses/inferences
}
SEARCH_EXPLOSION {
 MITIGATION := {
  Indexing,
  Subsumption,
  Ordering,
  SetOfSupport,
  UnitPreference,
  RelevanceFiltering,
  GivenClauseSelection
 }
}
INDEXING {
 index literals by predicate,polarity,term_structure
}

RESOLUTION_VS_MODUS_PONENS {
 ModusPonens := implication_elimination
 Resolution := clause_inference_using_complementary_literals
}
RESOLUTION_VS_NATURAL_DEDUCTION {
 Resolution := refutation_oriented_clause_calculus
 NaturalDeduction := introduction_elimination_calculus
}
RESOLUTION_VS_SAT {
 Resolution := clause_derivation_for_unsatisfiability
 SAT := commonly DPLL_CDCL_style_search
}
CDCL_RELATIONSHIP {
 learned_clauses MAY have resolution_proof_interpretations
}
THEOREM_PROVING {
 Axioms + NegatedConjecture
  -> Clausification
  -> ResolutionOrSuperposition
  -> EmptyClause
}
RESOLUTION_FAILURE {
 bounded_failure_to_derive_empty_clause
 DOES_NOT generally prove satisfiability in first-order logic
}
FAIRNESS {
 completeness_claim requires search eventually consider necessary eligible inferences
}

APPLICATION_RELATIONSHIPS {
 Resolution --supports--> AutomatedTheoremProving
 Resolution --supports--> LogicProgramming
 Resolution --supports--> DeductiveReasoning
 Resolution --supports--> FirstOrderLogic
 Resolution --supports--> PropositionalLogic
 Resolution --supports--> KnowledgeRepresentation
 Resolution --supports--> ArtificialIntelligence
 Resolution --supports--> FormalVerification
}

ONTOLOGY_LINKS {
 PARENT := LogicalReasoningOntology
 RELATED := {
  LogicalInferenceOntology,
  DeductiveReasoningOntology,
  RuleBasedReasoningOntology,
  PropositionalLogicOntology,
  PredicateLogicOntology,
  ClauseOntology,
  LiteralOntology,
  UnificationOntology,
  HornClauseOntology,
  LogicProgrammingOntology,
  SatisfiabilityOntology
 }
}

SEMANTIC_EQUIVALENCE {
 Resolution ≈ ResolutionRule
 Resolvent ≈ ClauseDerivedByResolution
 ResolutionRefutation ≈ RefutationByEmptyClause
 EmptyClause ≈ Contradiction WHEN clause_semantics
}

CONSTRAINTS {
 C1 := parents MUST contain complementary or unifiable complementary literals
 C2 := first-order resolution MUST apply substitutions consistently
 C3 := variables SHOULD be standardised apart before first-order resolution
 C4 := unification MUST respect occurs_check under standard finite-term semantics
 C5 := Skolemisation MUST be treated as equisatisfiability-preserving
 C6 := proof claims MUST preserve parent-clause provenance
 C7 := search restrictions MUST preserve required completeness conditions if claimed
 C8 := bounded failure to refute MUST NOT be presented as satisfiability proof
 C9 := equality reasoning MUST identify axioms/paramodulation/superposition
 C10 := simplification MUST preserve intended satisfiability/consequence properties
 C11 := SLD resolution MUST remain distinct from unrestricted first-order resolution
 C12 := every resolvent MUST be valid under selected calculus
}

REASONING_CHAIN Query Q {
 IDENTIFY goal
 IDENTIFY premises
 IDENTIFY propositional_or_first_order_context
 IDENTIFY resolution_calculus
 IDENTIFY search_strategy

 IF proving_entailment {
  ADD negated_goal
  CLAUSIFY
 }

 STANDARDISE variables_apart

 LOOP {
  SELECT parent_clauses
  SELECT complementary_literals

  IF first_order {
   COMPUTE MGU
   IF no_unifier: continue
  }

  DERIVE resolvent
  APPLY factoring
  APPLY simplification
  RECORD trace

  IF empty_clause {
   VERIFY_RESOLUTION_PROOF
   RETURN refutation_success
  }

  IF new_nonredundant_clause:
   ADD to clause_set

  IF saturation_or_resource_limit:
   BREAK
 }

 REPORT search_status_without_overclaiming
 VALIDATE constraints
 RETURN result WITH proof_or_search_trace
}

CONFIDENCE {
 PROPOSITIONAL_RESOLUTION_RULE := 1.00
 FIRST_ORDER_RESOLUTION_RULE := 1.00
 UNIFICATION_ROLE := 1.00
 REFUTATION_PRINCIPLE := 1.00
 PROPOSITIONAL_REFUTATION_COMPLETENESS := 1.00
 FIRST_ORDER_REFUTATION_COMPLETENESS := 0.99
 SLD_RELATIONSHIP := 1.00
 SPECIFIC_RESULT :=
  IF clauses_calculus_and_trace_complete THEN 1.00
  ELSE REQUIRE missing_information
}

UPDATE_MODEL {
 IMMUTABLE_CORE := {
  ClauseStructure,
  ComplementaryLiteralResolution,
  ResolventConstruction,
  RefutationByEmptyClause,
  UnificationForFirstOrderResolution
 }
 EXTENSIBLE := {
  ResolutionStrategies,
  ClauseSelection,
  LiteralSelection,
  SimplificationRules,
  EqualityCalculi,
  SLDResolution,
  Hyperresolution,
  IndexingMethods,
  ApplicationDomains,
  RelatedOntologies
 }
 ON_NEW_KNOWLEDGE {
  IDENTIFY new_clause
  STANDARDISE variables
  VALIDATE unification
  CHECK resolvent
  CHECK redundancy
  UPDATE clause_index
  UPDATE proof_dependencies
  UPDATE confidence
 }
}

AI_CONSUMPTION {
 MACHINE_READABLE := TRUE
 HUMAN_INTERPRETABLE := TRUE
 RECURSIVE_REASONING := TRUE
 ENTITY_RESOLUTION := TRUE
 CLAUSE_RESOLUTION := TRUE
 LITERAL_RESOLUTION := TRUE
 UNIFICATION_REASONING := TRUE
 RESOLVENT_GENERATION := TRUE
 REFUTATION_REASONING := TRUE
 CLAUSIFICATION_REASONING := TRUE
 SLD_REASONING := TRUE
 REDUNDANCY_REASONING := TRUE
 PROOF_TRACE_GENERATION := TRUE
 PROOF_VALIDATION := TRUE
 VALIDATION_REQUIRED := TRUE
}

FLOW_HASH {
 TARGET := TARGET_URL
 SUBJECT := "Resolution Ontology"
 VERSION := "1.0"
 CANONICAL_SIGNATURE := HASH(TARGET + SUBJECT + DOMAIN + VERSION)
}

OUTPUT {
 PRIMARY_ENTITY := Resolution
 INTERPRETATION := "Resolution is a clause-based inference rule that combines clauses containing complementary literals to derive resolvents. In first-order logic it works with unification and variable standardisation, and repeated resolution can establish unsatisfiability by deriving the empty clause, providing a core mechanism for automated theorem proving and logic programming."
}

END_FLOW