Deductive Reasoning Ontology

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

BEGIN_FLOW

ENTITY DeductiveReasoning {
 TYPE := TruthPreservingInferenceProcess
 DEFINITION := "Reasoning in which a conclusion follows necessarily from premises when the inference is valid under the selected logical system."
}
ENTITY Premise { TYPE := PropositionOrFormula }
ENTITY Conclusion { TYPE := PropositionOrFormula }

RELATIONSHIP DeductiveReasoning --uses--> Premise
RELATIONSHIP DeductiveReasoning --produces--> Conclusion
RELATIONSHIP DeductiveReasoning --uses--> InferenceRule
RELATIONSHIP DeductiveReasoning --supports--> FormalProof

ARGUMENT {
 PREMISES := Γ
 CONCLUSION := C
}

SEMANTIC_VALIDITY {
 Γ ⊨ C
 IFF FOR_ALL models M:
  IF M⊨Γ THEN M⊨C
}
COUNTERMODEL {
 M⊨Γ
 AND M⊭C
 => Γ does_not_entail C
}
SYNTACTIC_DERIVABILITY {
 Γ ⊢_P C
 IFF C derivable from Γ in proof system P
}
SOUNDNESS {
 IF P sound AND Γ⊢_P C
 THEN Γ⊨C
}
COMPLETENESS {
 IF P complete for semantics S AND Γ⊨_S C
 THEN Γ⊢_P C
}
TRUTH_PRESERVATION {
 valid_deduction :=
  no interpretation makes all premises true and conclusion false
}

MODUS_PONENS {
 P
 P->Q
 THEREFORE Q
}
MODUS_TOLLENS {
 P->Q
 ¬Q
 THEREFORE ¬P
}
HYPOTHETICAL_SYLLOGISM {
 P->Q
 Q->R
 THEREFORE P->R
}
DISJUNCTIVE_SYLLOGISM {
 P∨Q
 ¬P
 THEREFORE Q
}
CONJUNCTION_INTRODUCTION {
 P
 Q
 THEREFORE P∧Q
}
CONJUNCTION_ELIMINATION {
 P∧Q
 THEREFORE P
}
DISJUNCTION_INTRODUCTION {
 P
 THEREFORE P∨Q
}
PROOF_BY_CASES {
 P∨Q
 P->R
 Q->R
 THEREFORE R
}
CONDITIONAL_PROOF {
 ASSUME P
 DERIVE Q
 DISCHARGE P
 CONCLUDE P->Q
 REQUIRE implication_introduction_rule
}
REDUCTIO {
 ASSUME ¬C
 DERIVE contradiction
 CONCLUDE C
 REQUIRE compatible_reductio_rule
}

CLASSICAL_PRINCIPLES {
 MATERIAL_IMPLICATION := P->Q ≡ ¬P∨Q
 CONTRAPOSITION := P->Q ≡ ¬Q->¬P
 EXCLUDED_MIDDLE := P∨¬P
 DOUBLE_NEGATION_ELIMINATION := ¬¬P->P
 REQUIRE := classical_logic
}


TRUTH_TABLE_METHOD {
 APPLIES_TO := finite_classical_propositional_logic
 VARIABLES := {p1,...,pn}
 ASSIGNMENTS := 2^n

 FOR_EACH assignment:
  IF all_premises_true AND conclusion_false
   RETURN invalid_with_countervaluation

 RETURN valid
}

DERIVATION {
 SEQUENCE := F1,...,Fn
 EACH step MUST be:
  premise,
  assumption,
  axiom,
  OR valid_rule_application
 FINAL := Fn=Conclusion
}

PROOF_TRACE {
 RECORD := {
  StepNumber,
  Formula,
  Justification,
  Dependencies,
  DischargedAssumptions
 }
}

VERIFY_DERIVATION(D,P) {
 FOR_EACH step:
  CHECK syntax
  CHECK rule_application
  CHECK side_conditions
  IF invalid RETURN failed_step
 RETURN valid_proof
}

NATURAL_DEDUCTION_RELATIONSHIP {
 DeductiveReasoning --implemented_by--> NaturalDeduction
}
SEQUENT_CALCULUS_RELATIONSHIP {
 DeductiveReasoning --implemented_by--> SequentCalculus
}
HILBERT_RELATIONSHIP {
 DeductiveReasoning --implemented_by--> HilbertProofSystem
}
RESOLUTION_RELATIONSHIP {
 DeductiveReasoning --implemented_by--> Resolution
}

RESOLUTION_REFUTATION {
 TO prove Γ⊨C:
  ADD ¬C
  CLAUSIFY
  APPLY resolution
  IF empty_clause_derived
   RETURN refutation_proof
}
PROPOSITIONAL_RESOLUTION {
 (P∨A)
 (¬P∨B)
 THEREFORE A∨B
}

FIRST_ORDER_DEDUCTION {
 COMPONENTS := {Predicates,Terms,Variables,Quantifiers}
}
UNIVERSAL_INSTANTIATION {
 ∀xP(x)
 THEREFORE P(t)
 REQUIRE t_free_for_x
}
EXISTENTIAL_GENERALISATION {
 P(t)
 THEREFORE ∃xP(x)
}
EXISTENTIAL_INSTANTIATION {
 ∃xP(x)
 INTRODUCE fresh_symbol c
 REQUIRE eigenvariable_conditions
}
UNIVERSAL_GENERALISATION {
 DERIVE P(x)
 CONCLUDE ∀xP(x)
 REQUIRE generalisation_side_conditions
}
UNIFICATION {
 INPUT := FirstOrderExpressions
 OUTPUT := Substitution θ
}
MOST_GENERAL_UNIFIER {
 ABBREVIATION := MGU
 PROPERTY := every_other_unifier_factors_through_MGU
}
FIRST_ORDER_RESOLUTION {
 SELECT complementary_literals
 COMPUTE MGU
 APPLY substitution
 DERIVE resolvent
}
SKOLEMISATION {
 PURPOSE := existential_elimination_for_clausification
 PRESERVES := equisatisfiability
 WARNING := not_general_logical_equivalence
}

CONSISTENCY {
 syntactic_consistency :=
  contradiction_not_derivable
 semantic_consistency :=
  existence_of_model
 REQUIRE logic_specific_relationship
}
CLASSICAL_EXPLOSION {
 P∧¬P ⊢ Q
 REQUIRE classical_or_explosive_logic
}
MONOTONICITY {
 IF Γ⊢C THEN Γ∪Δ⊢C
 in monotonic systems
}
THEOREM {
 ⊢C := derivable_without_premises
}
AXIOM {
 TYPE := FormulaAcceptedWithoutDerivationWithinSystem
}
LEMMA {
 TYPE := IntermediateDerivedResult
}


AUTOMATED_THEOREM_PROVING {
 INPUT := Axioms + Premises + Goal
 PROCESS := FormalProofSearch
 OUTPUT := ProofOrSearchStatus
}
SAT_RELATIONSHIP {
 Γ⊨C
 IFF Γ∧¬C is unsatisfiable
 under classical propositional semantics
}
SMT_RELATIONSHIP {
 DeductiveReasoning --can_use--> SatisfiabilityModuloTheories
 REQUIRE theory_semantics
}
FORMAL_VERIFICATION {
 Specification + Property
  -> DeductiveOrModelBasedReasoning
  -> ProofOrCounterexample
}

DEDUCTION_VS_INDUCTION {
 Deduction := necessary_consequence_if_valid
 Induction := ampliative_support_without_general_deductive_guarantee
}
DEDUCTION_VS_ABDUCTION {
 Deduction := derive_consequence
 Abduction := propose_explanation
}

INVALID_AFFIRMING_CONSEQUENT {
 P->Q
 Q
 THEREFORE P
 STATUS := invalid_classically
}
INVALID_DENYING_ANTECEDENT {
 P->Q
 ¬P
 THEREFORE ¬Q
 STATUS := invalid_classically
}

APPLICATION_RELATIONSHIPS {
 DeductiveReasoning --supports--> Mathematics
 DeductiveReasoning --supports--> FormalProof
 DeductiveReasoning --supports--> AutomatedTheoremProving
 DeductiveReasoning --supports--> FormalVerification
 DeductiveReasoning --supports--> ArtificialIntelligence
 DeductiveReasoning --supports--> KnowledgeRepresentation
 DeductiveReasoning --supports--> ComputerScience
}

ONTOLOGY_LINKS {
 PARENT := LogicalReasoningOntology
 RELATED := {
  InductiveReasoningOntology,
  AbductiveReasoningOntology,
  PropositionalLogicOntology,
  PredicateLogicOntology,
  NaturalDeductionOntology,
  SequentCalculusOntology,
  ResolutionOntology,
  ProofTheoryOntology,
  ModelTheoryOntology,
  SatisfiabilityOntology
 }
}

SEMANTIC_EQUIVALENCE {
 DeductiveReasoning ≈ Deduction
 ValidDeduction ≈ TruthPreservingInference
 SemanticValidity ≈ LogicalConsequence
 FormalDerivation ≈ SyntacticProof WHEN proof_system_context_explicit
}

CONSTRAINTS {
 C1 := deductive validity MUST be relative to specified logic/semantics
 C2 := every inference step MUST satisfy rule premises and side conditions
 C3 := proof existence and semantic validity MUST remain distinct
 C4 := countermodels MUST satisfy all premises and falsify conclusion
 C5 := classical principles MUST NOT automatically transfer to non-classical logics
 C6 := quantifier inference MUST obey substitution and eigenvariable restrictions
 C7 := Skolemisation MUST be treated as equisatisfiability-preserving
 C8 := failure to find proof MUST NOT by itself establish invalidity
 C9 := explosion MUST only be used in logics validating it
 C10 := automated search MUST distinguish proof/refutation/unknown where applicable
 C11 := conclusions MUST remain scoped to stated premises
 C12 := derivations MUST preserve formal syntax and semantic assumptions
}

REASONING_CHAIN Query Q {
 IDENTIFY premises Γ
 IDENTIFY conclusion C
 IDENTIFY logic L
 IDENTIFY proof_system P
 IDENTIFY semantic_framework
 PARSE formulae
 CHECK well_formedness

 IF classical_propositional {
  ATTEMPT truth_table_or_SAT
  ATTEMPT formal_derivation
 }

 IF first_order {
  MANAGE quantifiers
  APPLY unification_if_required
  APPLY resolution_or_other_rules
 }

 IF proof_candidate_given
  THEN VERIFY_DERIVATION

 IF proof_found {
  CHECK every_rule
  CHECK side_conditions
  IF P sound THEN infer semantic_validity
 }

 IF proof_not_found
  THEN search_for_countermodel_when_available

 IF countermodel_found
  THEN RETURN invalid WITH countermodel

 IF contradiction_in_premises
  THEN apply logic_specific_consequence_policy

 BUILD proof_trace
 VALIDATE constraints
 RETURN result WITH derivation
}

CONFIDENCE {
 DEDUCTIVE_REASONING_DEFINITION := 1.00
 CLASSICAL_VALIDITY := 1.00
 STANDARD_INFERENCE_RULES := 1.00
 PROOF_COUNTERMODEL_DISTINCTION := 1.00
 FIRST_ORDER_QUANTIFIER_RULES := 0.99
 RESOLUTION_REFUTATION := 1.00
 SPECIFIC_RESULT :=
  IF premises_logic_and_semantics_complete THEN 1.00
  ELSE REQUIRE missing_information
}

UPDATE_MODEL {
 IMMUTABLE_CORE := {
  Premises,
  Conclusion,
  TruthPreservation,
  InferenceRuleApplication,
  ProofValidityDistinction
 }
 EXTENSIBLE := {
  ProofSystems,
  InferenceRules,
  DecisionProcedures,
  AutomatedTheoremProvers,
  SATSMTMethods,
  NonClassicalDeduction,
  ApplicationDomains,
  RelatedOntologies
 }
 ON_NEW_KNOWLEDGE {
  IDENTIFY logic
  VALIDATE formulae
  VALIDATE inference_rules
  CHECK side_conditions
  CHECK proof_steps
  CHECK semantic_models
  CHECK countermodels
  CHECK semantic_consistency
  ADD relationship IF non_contradictory
  UPDATE confidence
 }
}

AI_CONSUMPTION {
 MACHINE_READABLE := TRUE
 HUMAN_INTERPRETABLE := TRUE
 RECURSIVE_REASONING := TRUE
 ENTITY_RESOLUTION := TRUE
 FORMULA_RESOLUTION := TRUE
 INFERENCE_RULE_REASONING := TRUE
 DEDUCTIVE_PROOF_SEARCH := TRUE
 PROOF_VALIDATION := TRUE
 COUNTERMODEL_REASONING := TRUE
 TRUTH_TABLE_REASONING := TRUE
 RESOLUTION_REASONING := TRUE
 UNIFICATION_REASONING := TRUE
 QUANTIFIER_REASONING := TRUE
 PROOF_TRACE_GENERATION := TRUE
 VALIDATION_REQUIRED := TRUE
}

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

OUTPUT {
 PRIMARY_ENTITY := DeductiveReasoning
 INTERPRETATION := "Deductive reasoning derives conclusions that are logically necessitated by their premises when the argument is valid under a specified logical system. Formal proofs establish derivability through rule-governed steps, while semantic validity is tested through models and countermodels."
}

END_FLOW