Propositional Logic

# Propositional Logic — Flow Algebra

URL: https://kirethresearch.org/booksai-core/ontologies/mathematical-ontologies/mathematical-logic-ontologies/propositional-logic.html

FLOW PropositionalLogicOntology {

  DOMAIN:
    AI Core
    -> Ontologies
    -> Mathematical Ontologies
    -> Mathematical Logic Ontologies
    -> Propositional Logic

  PURPOSE:
    Represent propositional logic as a machine-interpretable formal system for reasoning over atomic propositions and truth-functional combinations of propositions. The ontology models propositional variables, truth values, logical connectives, well-formed formulas, syntax trees, valuations, truth tables, satisfiability, validity, tautologies, contradictions, contingencies, logical equivalence, normal forms, entailment, derivability, proof systems, Boolean functions, SAT reasoning, resolution, model checking, transformations, ambiguity, explainability, versioning and provenance. It enables AI systems to parse and normalise propositional expressions, evaluate them under valuations, compare formulas semantically, test satisfiability and validity, verify deductions and preserve strict distinctions between syntax and semantics, implication and causation, satisfiability and validity, equivalence and syntactic identity, and proof search versus proof verification.

  ENTITY PropositionalLogic {
    TYPE: TruthFunctionalFormalLogic

    PROPERTIES:
      has_atomic_propositions
      has_truth_values
      has_connectives
      has_formulas
      has_valuations
      has_truth_tables
      supports_satisfiability
      supports_validity
      supports_entailment
      supports_equivalence
      supports_formal_proofs
      supports_SAT_reasoning
  }

  ENTITY PropositionalVariable {
    TYPE: AtomicFormulaSymbol

    PROPERTIES:
      identifier
      symbol
      truth_assignment
  }

  ENTITY PropositionalFormula {
    TYPE: RecursivelyConstructedFormula

    COMPONENTS:
      atomic_propositions
      connectives
      syntax_tree
  }

  ENTITY Valuation {
    TYPE: TruthAssignment

    MAPPING:
      propositional_variables -> truth_values
  }

  LANGUAGE_MODEL {
    alphabet:
      propositional_variables
      connective_symbols
      parentheses
      truth_constants_whenavailable

    RULE:
      language_identifier_andnotation_profile SHOULD be preserved
  }

  ATOMIC_PROPOSITION_MODEL {
    atom:
      indivisible_atpropositional_level

    RULE:
      internal_natural_language_orpredicate_structure_isnotanalysed_atthislogical_level
  }

  PROPOSITIONAL_VARIABLE_MODEL {
    possible:
      p
      q
      r
      P_1...P_n

    RULE:
      variable_symbol != proposition_meaning_withoutinterpretation
  }

  TRUTH_VALUE_MODEL {
    classical:
      TRUE
      FALSE

    RULE:
      this_ontology_defaults_toclassical_two_valued_semantics_unlessextension_declared
  }

  TRUTH_CONSTANT_MODEL {
    possible:
      top
      bottom
      TRUE
      FALSE

    RULE:
      truth_constant != propositional_variable
  }

  FORMULA_FORMATION_MODEL {
    base:
      every_propositional_variable_isformula

    recursive:
      if_A_formula_then_NOT_A_formula
      if_A_B_formulas_then_binary_connective_of_A_B_isformula

    RULE:
      formula_generation MUST followdeclared_grammar
  }

  WELL_FORMED_FORMULA_MODEL {
    abbreviation:
      WFF

    condition:
      conforms_toformation_rules

    RULE:
      well_formedness != truth_orvalidity
  }

  TOKENISATION_MODEL {
    input:
      propositional_expression

    tokens:
      atoms
      operators
      parentheses
      constants

    RULE:
      multi_character_operators MUST remain_atomic
  }

  PARSER_MODEL {
    input:
      tokens

    output:
      abstract_syntax_tree

    RULE:
      parser MUST respectparentheses_precedence_andassociativity
  }

  ABSTRACT_SYNTAX_TREE_MODEL {
    leaves:
      propositional_variables_ortruth_constants

    internal_nodes:
      connectives

    RULE:
      AST != truth_table_orsemantic_model
  }

  PRECEDENCE_MODEL {
    common_default:
      NOT
      AND
      OR
      IMPLIES
      IFF

    RULE:
      actual_precedence MUST followdeclared_notation
  }

  ASSOCIATIVITY_MODEL {
    operators:
      may_have declared_associativity

    RULE:
      implication_chain MUST not_be parsed_withoutdeclared_associativity_orparentheses
  }

  PARENTHESIS_MODEL {
    role:
      explicit_grouping

    RULE:
      parentheses_override_default_precedence
  }

  CONNECTIVE_MODEL {
    possible:
      negation
      conjunction
      disjunction
      implication
      biconditional
      exclusive_OR
      NAND
      NOR

    RULE:
      connective_arity_andtruth_function MUST be explicit
  }

  NEGATION_MODEL {
    notation:
      NOT A
      ¬A

    truth_function:
      TRUE -> FALSE
      FALSE -> TRUE
  }

  CONJUNCTION_MODEL {
    notation:
      A AND B
      A ∧ B

    true_when:
      A=TRUE
      AND B=TRUE
  }

  DISJUNCTION_MODEL {
    notation:
      A OR B
      A ∨ B

    classical_default:
      inclusive_OR

    false_when:
      A=FALSE
      AND B=FALSE
  }

  EXCLUSIVE_OR_MODEL {
    notation:
      A XOR B

    true_when:
      exactly_one_ofA_B_isTRUE
  }

  IMPLICATION_MODEL {
    notation:
      A -> B
      A → B

    false_when:
      A=TRUE
      AND B=FALSE

    classical_equivalence:
      NOT A OR B

    RULE:
      material_implication != causal_relation
  }

  BICONDITIONAL_MODEL {
    notation:
      A <-> B
      A ↔ B

    true_when:
      A_andB_have_same_truth_value
  }

  NAND_MODEL {
    definition:
      NOT(A AND B)

    RULE:
      NAND_isfunctionally_complete
  }

  NOR_MODEL {
    definition:
      NOT(A OR B)

    RULE:
      NOR_isfunctionally_complete
  }

  CONNECTIVE_ARITY_MODEL {
    unary:
      NOT

    binary:
      AND
      OR
      XOR
      IMPLIES
      IFF
      NAND
      NOR

    RULE:
      wrong_operand_count MUST be flagged
  }

  TRUTH_FUNCTION_MODEL {
    connective:
      deterministic_mapping_fromoperand_truth_values_toresult

    RULE:
      truth_function_identity SHOULD be canonicalised
  }

  VALUATION_MODEL {
    v:
      atoms -> {TRUE,FALSE}

    extension:
      recursively_evaluate_compound_formulas

    RULE:
      every_atom_informula MUST receive_value_forcomplete_evaluation
  }

  PARTIAL_VALUATION_MODEL {
    assignment:
      subset_ofatoms_havevalues

    RULE:
      formula_value MAY remainundetermined
  }

  TRUTH_EVALUATION_MODEL {
    process:
      evaluate_AST_bottom_up_under valuation

    RULE:
      evaluation MUST useconnective_truth_functions
  }

  TRUTH_TABLE_MODEL {
    atoms:
      n

    rows:
      2^n

    columns:
      atoms
      optional_subformulas
      target_formula

    RULE:
      exhaustive_table_requires_allvaluations
  }

  TRUTH_TABLE_ROW_MODEL {
    fields:
      valuation
      subformula_values
      formula_value
  }

  TAUTOLOGY_MODEL {
    formula:
      TRUE_underallvaluations

    RULE:
      tautology == propositional_validity_underclassical_semantics
  }

  CONTRADICTION_MODEL {
    formula:
      FALSE_underallvaluations

    RULE:
      contradiction != contingent_falsehood
  }

  CONTINGENCY_MODEL {
    formula:
      TRUE_undersome_valuations
      FALSE_underothers
  }

  SATISFIABILITY_MODEL {
    formula:
      satisfiable_ifexistsvaluation_withTRUE

    RULE:
      satisfiable != valid
  }

  UNSATISFIABILITY_MODEL {
    formula:
      FALSE_underallvaluations

    RULE:
      unsatisfiable_formula_iscontradiction_underclassical_propositional_semantics
  }

  VALIDITY_MODEL {
    formula:
      valid_ifTRUE_underallvaluations

    RULE:
      valid != satisfiable_only
  }

  FALSIFIABILITY_MODEL {
    formula:
      falsifiable_ifexistsvaluation_withFALSE

    RULE:
      falsifiable != unsatisfiable
  }

  MODEL_MODEL {
    valuation:
      model_offormula_ifformula_TRUE

    RULE:
      propositional_model == satisfying_valuation_underthiscontext
  }

  COUNTERMODEL_MODEL {
    valuation:
      makes_candidate_valid_formula_FALSE

    RULE:
      one_countermodel_refutes_validity
  }

  LOGICAL_EQUIVALENCE_MODEL {
    A:
      equivalent_toB

    condition:
      forallvaluations v:
        v(A)=v(B)

    RULE:
      equivalence != syntactic_identity
  }

  SYNTACTIC_IDENTITY_MODEL {
    formulas:
      same_resolved_AST

    RULE:
      syntactic_identity_isstronger_thansemantic_equivalence_asrepresentation_relation
  }

  DOUBLE_NEGATION_MODEL {
    classical:
      NOT NOT A
      equivalent_to
      A
  }

  DE_MORGAN_MODEL {
    NOT(A AND B)
      equivalent_to
      NOT A OR NOT B

    NOT(A OR B)
      equivalent_to
      NOT A AND NOT B
  }

  COMMUTATIVITY_MODEL {
    A AND B
      equivalent_to
      B AND A

    A OR B
      equivalent_to
      B OR A
  }

  ASSOCIATIVITY_EQUIVALENCE_MODEL {
    (A AND B) AND C
      equivalent_to
      A AND (B AND C)

    (A OR B) OR C
      equivalent_to
      A OR (B OR C)
  }

  DISTRIBUTIVITY_MODEL {
    A AND (B OR C)
      equivalent_to
      (A AND B) OR (A AND C)

    A OR (B AND C)
      equivalent_to
      (A OR B) AND (A OR C)
  }

  IDEMPOTENCE_MODEL {
    A AND A equivalent_to A
    A OR A equivalent_to A
  }

  ABSORPTION_MODEL {
    A OR (A AND B) equivalent_to A
    A AND (A OR B) equivalent_to A
  }

  COMPLEMENT_MODEL {
    A OR NOT A equivalent_to TRUE
    A AND NOT A equivalent_to FALSE
  }

  IMPLICATION_ELIMINATION_MODEL {
    A -> B
      equivalent_to
      NOT A OR B
  }

  BICONDITIONAL_ELIMINATION_MODEL {
    A <-> B
      equivalent_to
      (A -> B) AND (B -> A)
  }

  CONTRAPOSITION_MODEL {
    A -> B
      equivalent_to
      NOT B -> NOT A

    RULE:
      equivalence_isclassical
  }

  NORMAL_FORM_MODEL {
    possible:
      NNF
      CNF
      DNF

    RULE:
      normal_form_type MUST be explicit
  }

  NEGATION_NORMAL_FORM_MODEL {
    abbreviation:
      NNF

    condition:
      NOT_occurs_only_directly_beforeatoms
  }

  CONJUNCTIVE_NORMAL_FORM_MODEL {
    abbreviation:
      CNF

    structure:
      conjunction_ofclauses
  }

  DISJUNCTIVE_NORMAL_FORM_MODEL {
    abbreviation:
      DNF

    structure:
      disjunction_ofterms_orconjunctions_ofliterals
  }

  LITERAL_MODEL {
    possible:
      atom
      negated_atom
  }

  CLAUSE_MODEL {
    structure:
      disjunction_ofliterals
  }

  TERM_IN_DNF_MODEL {
    structure:
      conjunction_ofliterals

    RULE:
      DNF_term != logical_language_term
  }

  CNF_TRANSFORMATION_MODEL {
    common_steps:
      eliminate_IFF
      eliminate_implication
      push_negation
      distribute_OR_overAND

    RULE:
      transformation MUST preserveequivalence_whenusingdirect_boolean_rewrites
  }

  DNF_TRANSFORMATION_MODEL {
    common_steps:
      eliminate_IFF
      eliminate_implication
      push_negation
      distribute_AND_overOR
  }

  TSEITIN_TRANSFORMATION_MODEL {
    source:
      arbitrary_formula

    target:
      CNF_withauxiliary_variables

    property:
      equisatisfiable

    RULE:
      equisatisfiable != logically_equivalent_overextended_vocabulary
  }

  CANONICAL_DNF_MODEL {
    form:
      disjunction_ofminterms_forTRUE_rows

    RULE:
      atom_order MUST be fixed
  }

  CANONICAL_CNF_MODEL {
    form:
      conjunction_ofmaxterms_forFALSE_rows

    RULE:
      atom_order MUST be fixed
  }

  MINTERM_MODEL {
    conjunction:
      contains_each_atom_once_aspositive_ornegative

    corresponds_to:
      one_valuation
  }

  MAXTERM_MODEL {
    disjunction:
      contains_each_atom_once_aspositive_ornegative

    corresponds_to:
      one_false_row_undercanonical_convention
  }

  BOOLEAN_FUNCTION_MODEL {
    function:
      {0,1}^n -> {0,1}

    RULE:
      formulas MAY represent_same_boolean_function
  }

  FUNCTIONAL_COMPLETENESS_MODEL {
    connective_set:
      functionally_complete_ifcanexpress_every_boolean_function

    examples:
      {NOT,AND}
      {NOT,OR}
      {NAND}
      {NOR}

    RULE:
      completeness_here != proof_system_completeness
  }

  DUALITY_MODEL {
    operation:
      interchange_AND_OR
      interchange_TRUE_FALSE

    RULE:
      duality_relation MUST preserve_declared_negation_convention
  }

  SEMANTIC_ENTAILMENT_MODEL {
    Gamma entails A:
      everyvaluation_satisfying_allGamma_satisfiesA

    RULE:
      entailment != material_implication_asbinary_formula
  }

  FINITE_ENTAILMENT_MODEL {
    premises:
      A_1...A_n

    equivalence:
      Gamma entails B
      iff
      conjunction(Gamma) -> B_isvalid

    RULE:
      empty_premise_case MUST be handled
  }

  COUNTEREXAMPLE_TO_ENTAILMENT_MODEL {
    valuation:
      allpremises_TRUE
      conclusion_FALSE

    RULE:
      one_suchvaluation_refutes_entailment
  }

  ARGUMENT_MODEL {
    premises:
      Gamma

    conclusion:
      C

    valid_if:
      Gamma entails C
  }

  SOUND_ARGUMENT_MODEL {
    requirements:
      valid
      premises_true_underintended_interpretation

    RULE:
      propositional_validity_alone_doesnotestablish_actual_premise_truth
  }

  INFERENCE_RULE_MODEL {
    possible:
      modus_ponens
      modus_tollens
      hypothetical_syllogism
      disjunctive_syllogism
      conjunction
      simplification
      addition
      resolution

    RULE:
      rule_validity MUST be established_underlogic
  }

  MODUS_PONENS_MODEL {
    A
    A -> B
    therefore B
  }

  MODUS_TOLLENS_MODEL {
    A -> B
    NOT B
    therefore NOT A
  }

  HYPOTHETICAL_SYLLOGISM_MODEL {
    A -> B
    B -> C
    therefore A -> C
  }

  DISJUNCTIVE_SYLLOGISM_MODEL {
    A OR B
    NOT A
    therefore B
  }

  CONJUNCTION_RULE_MODEL {
    A
    B
    therefore A AND B
  }

  SIMPLIFICATION_RULE_MODEL {
    A AND B
    therefore A
  }

  ADDITION_RULE_MODEL {
    A
    therefore A OR B
  }

  RESOLUTION_RULE_MODEL {
    A OR C
    NOT A OR D
    therefore C OR D
  }

  FALLACY_MODEL {
    possible:
      affirming_consequent
      denying_antecedent

    RULE:
      invalid_pattern MAY stillhaveinstances_withtrueconclusion
  }

  AFFIRMING_CONSEQUENT_MODEL {
    A -> B
    B
    therefore A

    status:
      invalid
  }

  DENYING_ANTECEDENT_MODEL {
    A -> B
    NOT A
    therefore NOT B

    status:
      invalid
  }

  PROOF_SYSTEM_MODEL {
    components:
      axioms_orassumptions
      inference_rules
      derivation_definition

    RULE:
      proof_system != semantic_truth_table_method
  }

  DERIVABILITY_MODEL {
    Gamma proves A:
      formal_derivation_exists

    RULE:
      syntactic_derivability != semantic_entailment_bydefinition
  }

  SOUNDNESS_MODEL {
    proof_system:
      Gamma_proves_A
      implies
      Gamma_entails_A
  }

  COMPLETENESS_MODEL {
    proof_system:
      Gamma_entails_A
      implies
      Gamma_proves_A

    RULE:
      completeness_claim MUST identify_proof_system
  }

  CONSISTENCY_MODEL {
    formula_set:
      satisfiable_underclassical_propositional_semantics

    syntactic_variant:
      does_notderive_contradiction

    RULE:
      semantic_and syntactic_definitions SHOULD be distinguished
  }

  PROOF_BY_TRUTH_TABLE_MODEL {
    method:
      enumerate_valuations

    RULE:
      finite_andcomplete_forfinite_propositional_formulas
  }

  PROOF_BY_EQUIVALENCE_MODEL {
    method:
      transform_formula_usingvalid_equivalences

    RULE:
      every_transformation MUST preserveequivalence
  }

  PROOF_BY_DEDUCTION_MODEL {
    method:
      apply_inference_rules

    RULE:
      proof_steps MUST be justified
  }

  PROOF_BY_CONTRADICTION_MODEL {
    method:
      add_negation_ofgoal
      derivecontradiction

    RULE:
      classical_context MUST be explicit
  }

  RESOLUTION_REFUTATION_MODEL {
    process:
      premises_plusnegated_goal
      convert_toCNF
      resolve
      derive_empty_clause

    RULE:
      empty_clause_certifies_unsatisfiability_underresolution_system
  }

  SAT_PROBLEM_MODEL {
    input:
      propositional_formula

    question:
      exists_satisfying_valuation
  }

  UNSAT_PROBLEM_MODEL {
    input:
      propositional_formula

    question:
      no_satisfying_valuation_exists
  }

  SAT_ASSIGNMENT_MODEL {
    valuation:
      satisfies_formula

    RULE:
      assignment SHOULD be retained_aswitness
  }

  SAT_SOLVER_MODEL {
    input:
      formula_usually_CNF_orinternal_rep
resentation

    possible_output:
      SAT_withassignment
      UNSAT_withcertificate_whenavailable
      UNKNOWN_whenapplicable

    RULE:
      solver_status MUST be preserved
  }

  DPLL_MODEL {
    process:
      unit_propagation
      pure_literal_optional
      branching
      backtracking

    RULE:
      implementation_strategy != logical_semantics
  }

  CDCL_MODEL {
    process:
      decision
      propagation
      conflict_analysis
      clause_learning
      backjumping

    RULE:
      learned_clauses MUST be logical_consequences_underalgorithm_invariant
  }

  UNIT_CLAUSE_MODEL {
    clause:
      one_literal
  }

  UNIT_PROPAGATION_MODEL {
    unit_literal:
      forces_truth_assignment_tosatisfyclause

    RULE:
      contradictions MUST be detected
  }

  PURE_LITERAL_MODEL {
    atom:
      occurs_onlyonepolarity_informula

    RULE:
      pure_literal_elimination_preserves_satisfiability
  }

  RESOLUTION_MODEL {
    clauses:
      C OR p
      D OR NOT p

    resolvent:
      C OR D

    RULE:
      tautological_resolvents MAY be discarded_underappropriate procedure
  }

  EMPTY_CLAUSE_MODEL {
    clause:
      contains_no_literals

    semantics:
      FALSE

    RULE:
      derivation_ofempty_clause_signals_unsatisfiability
  }

  SAT_CERTIFICATE_MODEL {
    SAT:
      satisfying_assignment

    UNSAT:
      proof_orcertificate_whenavailable

    RULE:
      certificate_checker SHOULD be identified
  }

  MODEL_COUNTING_MODEL {
    problem:
      count_satisfying_valuations

    notation:
      sharp_SAT

    RULE:
      count != probability_withoutdistribution
  }

  MAX_SAT_MODEL {
    objective:
      maximise_number_orweight_ofsatisfied_clauses

    RULE:
      MAX_SAT != SAT_decision_problem
  }

  WEIGHTED_SAT_MODEL {
    clauses_orassignments:
      carry_weights

    RULE:
      weight_semantics MUST be explicit
  }

  HORN_FORMULA_MODEL {
    clause:
      atmostone_positive_literal

    RULE:
      Horn_fragment_has_special_algorithmic_properties
  }

  HORN_REASONING_MODEL {
    process:
      forward_chaining_orlinear_time_algorithms_understandard_setting

    RULE:
      fragment_identification MUST be validated
  }

  TWO_SAT_MODEL {
    formula:
      CNF_withatmosttwo_literals_perclause

    RULE:
      2_SAT != general_SAT_complexity
  }

  IMPLICATION_GRAPH_MODEL {
    for_2SAT:
      nodes:
        literals
      edges:
        implications_fromclauses

    RULE:
      satisfiability_can_be tested_viastrongly_connected_components
  }

  BOOLEAN_CIRCUIT_MODEL {
    gates:
      AND
      OR
      NOT
      other_boolean_functions

    RULE:
      circuit_andformula_are_related_butrepresentation_differs
  }

  CIRCUIT_SAT_MODEL {
    input:
      Boolean_circuit

    question:
      exists_input_makingoutput_TRUE

    RULE:
      circuit_SAT_andformula_SAT_arepolynomially_related_butnotidentical_representation
  }

  BINARY_DECISION_DIAGRAM_MODEL {
    abbreviation:
      BDD

    representation:
      decision_graph_forBoolean_function

    RULE:
      variable_order_materially_affects_size
  }

  REDUCED_ORDERED_BDD_MODEL {
    abbreviation:
      ROBDD

    property:
      canonical_forfixed_variable_order

    RULE:
      canonicality_requires_reduction_andfixed_order
  }

  BOOLEAN_ALGEBRA_LINK_MODEL {
    mapping:
      FALSE -> 0
      TRUE -> 1
      AND -> meet_or multiplication_underBoolean_encoding
      OR -> join
      NOT -> complement

    RULE:
      algebraic_representation MUST preserve_boolean_semantics
  }

  SET_ALGEBRA_LINK_MODEL {
    undercharacteristic_mapping:
      AND -> intersection
      OR -> union
      NOT -> complement

    RULE:
      universe_ofdiscourse MUST be specified
  }

  DIGITAL_LOGIC_LINK_MODEL {
    propositions:
      maymap_toBoolean_signals

    RULE:
      physical_voltage_state != abstract_truth_value
  }

  PROBABILITY_DISTINCTION_MODEL {
    truth_value:
      TRUE_orFALSE_undervaluation

    probability:
      measure_overpossible_valuations_or events

    RULE:
      probability_ofproposition != truth_value
  }

  FUZZY_LOGIC_DISTINCTION_MODEL {
    fuzzy_truth_degree:
      graded

    propositional_classical_truth:
      binary

    RULE:
      fuzzy_degree != classical_truth_probability
  }

  THREE_VALUED_EXTENSION_MODEL {
    possible:
      TRUE
      FALSE
      UNKNOWN

    RULE:
      truth_tables MUST be separatelydefined
      andmust_not_be silentlytreated_asclassical
  }

  PARACONSISTENT_EXTENSION_MODEL {
    semantics:
      maypermitinconsistent_information_withoutexplosion

    RULE:
      classical_equivalences MAY fail
  }

  INTUITIONISTIC_PROPOSITIONAL_MODEL {
    proof_semantics:
      constructive

    RULE:
      excluded_middle_anddouble_negation_elimination_notgenerally_available
  }

  CLASSICAL_PROPOSITIONAL_MODEL {
    semantics:
      Boolean_two_valued_truth_functions

    RULE:
      allclassical_equivalence_rules_assume_thiscontext
  }

  KRIPKE_EXTENSION_DISTINCTION_MODEL {
    intuitionistic_or modal:
      truth_maydepend_onworld_orstate

    RULE:
      notpart_ofbasic_classical_valuation_semantics
  }

  NATURAL_LANGUAGE_FORMALISATION_MODEL {
    source:
      natural_language_statement

    target:
      propositional_formula

    process:
      identify_atomic_claims
      negation
      conjunction
      disjunction
      conditionals
      biconditionals

    RULE:
      formalisation_isinterpretive
  }

  ATOM_SELECTION_MODEL {
    source_claim:
      choosepropositional_atoms

    RULE:
      atoms SHOULD preservemeaning_relevant_toreasoning_task
  }

  CONDITIONAL_FORMALISATION_MODEL {
    phrases:
      if_A_then_B
      A_only_if_B
      A_if_B
      A_if_and_only_if_B

    RULE:
      linguistic_direction MUST be resolved_carefully
  }

  ONLY_IF_MODEL {
    "A only if B":
      A -> B
  }

  IF_MODEL {
    "A if B":
      B -> A
  }

  NECESSARY_CONDITION_MODEL {
    B_necessary_for_A:
      A -> B
  }

  SUFFICIENT_CONDITION_MODEL {
    A_sufficient_for_B:
      A -> B
  }

  UNLESS_MODEL {
    common_classical_form:
      unless_A_B
      maymap_to
      NOT A -> B
      or A OR B
      depending_syntax

    RULE:
      natural_language_context MUST be resolved
  }

  SCOPE_AMBIGUITY_MODEL {
    source:
      negation_orconnective_scope_unclear

    RULE:
      preserve_candidate_formulas
  }

  INCLUSIVE_EXCLUSIVE_OR_AMBIGUITY_MODEL {
    source:
      natural_language_or

    RULE:
      default_assumption MUST be explicit_orambiguity_preserved
  }

  IMPLICATION_AMBIGUITY_MODEL {
    source:
      causal_predictive_normative_or material_conditional_language

    RULE:
      propositional_formalisation MUST notclaimcausality
  }

  FORMALISATION_CONFIDENCE_MODEL {
    confidence:
      support_forchosen_atomisation_andconnective_structure

    RULE:
      confidence != truth
  }

  SEMANTIC_EQUIVALENCE_MODEL {
    formulas:
      compare_truth_vectors_overallvaluations

    RULE:
      identical_truth_vector establishes_classical_propositional_equivalence
  }

  TRUTH_VECTOR_MODEL {
    formula:
      ordered_sequence_oftruth_values_overfixedvaluation_order

    RULE:
      valuation_order MUST be recorded
  }

  HASH_MODEL {
    semantic_hash:
      mayderive_fromcanonical_truth_vector_orcanonical_normal_form

    RULE:
      hash_method_andatom_order MUST be explicit
  }

  FORMULA_SIMPLIFICATION_MODEL {
    goal:
      reduce_formula_size_orcomplexity

    RULE:
      simplification MUST preserveequivalence_unlessdeclared_equisatisfiable_only
  }

  CONSTANT_PROPAGATION_MODEL {
    examples:
      A AND TRUE -> A
      A OR FALSE -> A
      A AND FALSE -> FALSE
      A OR TRUE -> TRUE

    RULE:
      rewrite_isclassically_equivalent
  }

  SUBSUMPTION_MODEL {
    CNF:
      if_clause_C_subset_clause_D
      then_D_mayberemoved

    RULE:
      clause_representation MUST be set_orappropriatelynormalised
  }

  TAUTOLOGICAL_CLAUSE_MODEL {
    clause:
      contains_A_andNOT_A

    semantics:
      always_TRUE

    RULE:
      mayberemoved_fromCNF_withoutchangingformula_truth
  }

  DUPLICATE_LITERAL_MODEL {
    clause:
      repeated_literal

    RULE:
      duplicates_canberemoved_underBoolean_idempotence
  }

  PROOF_CERTIFICATE_MODEL {
    artifact:
      truth_table
      derivation
      resolution_refutation
      SAT_certificate
      BDD_equivalence

    RULE:
      certificate_type MUST be explicit
  }

  PROOF_CHECKER_MODEL {
    input:
      formula
      certificate

    output:
      verified_orrejected

    RULE:
      checker_version SHOULD be preserved
  }

  AUTOMATED_REASONING_MODEL {
    AI:
      parse
      evaluate
      simplify
      normalise
      test_SAT
      test_validity
      test_entailment
      compare_equivalence
      constructproof
      explain

    RULE:
      solver_orheuristic_result MUST preserveverification_status
  }

  HEURISTIC_MODEL {
    purpose:
      choosebranching_variable_rewrite_orproof_strategy

    RULE:
      heuristic_choice != logical_inference
  }

  UNKNOWN_STATUS_MODEL {
    possible:
      unknown
      timeout
      resource_limit
      parse_ambiguity

    RULE:
      unknown != FALSE
      unknown != UNSAT
  }

  EXPLAINABILITY_MODEL {
    output:
      source_formula
      parsed_AST
      atoms
      valuations_orcounterexample
      transformations
      proof_orcertificate
      result

    RULE:
      explanation MUST distinguishsemantic_test_fromsyntactic_proof
  }

  DEPENDENCY_MODEL {
    derived_formula:
      depends_on
        source_formula
        rewrite_rules
        premises
        inference_rules

    RULE:
      transformations MUST be traceable
  }

  VERSION_MODEL {
    versioned:
      language
      notation
      proof_system
      SAT_solver
      transformation_rules
      ontology

    RULE:
      reasoning_record MUST preserveversions
  }

  PROVENANCE_MODEL {
    fields:
      source
      formalisation
      parser
      proof_system
      solver
      certificate
      version
      agent

    RULE:
      propositional_result MUST remain_provenance_linked
  }

  INTEROPERABILITY_MODEL {
    exchange:
      atom_identifiers
      formula_AST
      connective_identifiers
      valuations
      CNF_orDNF
      proof_certificate
      result_status

    RULE:
      surface_formula_string_alone MAY beambiguous
  }

  KNOWLEDGE_GRAPH_MODEL {
    nodes:
      atom
      formula
      connective
      valuation
      clause
      proof
      SAT_result

    edges:
      CONTAINS
      NEGATES
      EQUIVALENT_TO
      ENTAILS
      SATISFIED_BY
      REFUTED_BY
      DERIVED_FROM
      TRANSFORMS_TO

    RULE:
      semantic_and syntactic_edges MUST be distinguished
  }

  RELATIONSHIPS {
    PropositionalLogic -> CONTAINS -> PropositionalFormula
    PropositionalFormula -> CONTAINS -> PropositionalVariable
    PropositionalFormula -> USES -> Connective
    Valuation -> ASSIGNS -> TruthValue
    Valuation -> SATISFIES -> PropositionalFormula
    Countermodel -> REFUTES -> ValidityClaim
    Formula -> MAY_TRANSFORM_TO -> NormalForm
    Proof -> DERIVES -> Formula
    SATCertificate -> SUPPORTS -> SATResult
  }

  SEMANTIC_EQUIVALENCE {
    "propositional logic" ~= truth_functional_logic_overatomic_propositions
    "propositional formula" ~= recursively_constructed_expression_fromatoms_andconnectives
    "valuation" ~= assignment_oftruth_values_toatomic_propositions

    atom != internal_predicate_structure
    well_formedness != truth
    satisfiable != valid
    falsifiable != unsatisfiable
    equivalence != syntactic_identity
    implication != causation
    entailment != material_implication
    proof_system != truth_table_semantics
    derivability != entailment_bydefinition
    equisatisfiable != logically_equivalent
    probability != truth_value
    heuristic_choice != inference_rule
  }

  CONSTRAINTS {
    propositional_atoms_must_have_stable_identifiers = true
    formula_parse_structure_must_be preserved = true
    connective_arity_andtruth_functions_must_be explicit = true
    parentheses_precedence_andassociativity_must_be respected = true
    satisfiability_validity_falsifiability_andunsatisfiability_must_be distinguished = true
    semantic_equivalence_and syntactic_identity_must_be distinguished = true
    implication_must_not_be interpreted_ascausation = true
    entailment_andmaterial_implication_must_be distinguished = true
    derivability_andsemantic_entailment_must_be distinguished = true
    normal_form_transformations_must_record_equivalence_orequisatisfiability_status = true
    SAT_witnesses_andcountermodels_should_be preserved = true
    natural_language_formalisation_ambiguity_must_be preserved = true
    solver_unknown_timeout_orresource_limit_must_not_be interpreted_asfalse_orUNSAT = true
    provenance_must_be preserved = true
  }

  PROPOSITIONAL_LOGIC_RECORD_MODEL {
    RECORD:
      formula_identifier
      language_identifier
      notation_profile
      source_expression
      atom_identifiers
      token_sequence
      syntax_tree
      connective_structure
      valuation
      truth_value
      truth_vector
      truth_table_identifier
      satisfiability_status
      validity_status
      falsifiability_status
      countermodel
      equivalent_formula_identifiers
      normal_form_type
      CNF
      DNF
      clauses
      premises
      conclusion
      entailment_status
      derivability_status
      proof_identifier
      proof_steps
      SAT_solver_identifier
      SAT_status
      SAT_assignment
      proof_certificate
      formalisation_confidence
      ambiguity_status
      version
      provenance

    RULE:
      propositional_logic_record MUST support_reconstruction_ofsyntax_semantics_valuations_transformations_proof_andprovenance
  }

  REASONING_RULES {
    IF propositional_expression_received
      THEN tokenise
      parse_AST
      identify_atoms_andconnectives
      validate_well_formedness

    IF valuation_supplied
      THEN evaluate_formula_bottom_up

    IF validity_requested
      THEN enumerate_truth_table_whenfeasible
      orsolve_NOT_formula_forUNSAT
      andpreserve_countermodel_iffound

    IF satisfiability_requested
      THEN search_forvaluation
      preserve_assignment_ifSAT
      preserve_certificate_ifUNSAT_andavailable

    IF equivalence_requested
      THEN test_XOR_orbiconditional_validity
      orcompare_truth_vectors
      underfixed_atom_mapping

    IF entailment_requested
      THEN test_premises_AND_NOT_conclusion_forunsatisfiability
      andpreserve_counterexample_ifSAT

    IF normal_form_requested
      THEN apply_declared_transformations
      record_equivalent_orequisatisfiable_status

    IF natural_language_statement_received
      THEN identify_candidate_atoms_andconnective_structure
      preserve_ambiguity_andformalisation_confidence

    IF solver_returns_unknown_timeout_orresource_limit
      THEN preserve_status
      anddo_notinfer_false_invalid_orUNSAT

    IF formula_orproof_system_revision_occurs
      THEN preserve_previous_record
      revalidate_current_results_underdeclared_version
  }

  VALIDATION {
    CHECK formula_identifier
    CHECK language
    CHECK notation
    CHECK tokenisation
    CHECK syntax_tree
    CHECK well_formedness
    CHECK atom_identifiers
    CHECK connective_arity
    CHECK precedence_andassociativity
    CHECK valuation_completeness
    CHECK truth_evaluation
    CHECK truth_table
    CHECK satisfiability
    CHECK validity
    CHECK falsifiability
    CHECK countermodel
    CHECK logical_equivalence
    CHECK normal_form
    CHECK CNF_DNF_structure
    CHECK entailment
    CHECK derivability
    CHECK proof_steps
    CHECK SAT_status
    CHECK SAT_assignment_orcertificate
    CHECK formalisation_ambiguity
    CHECK version
    CHECK provenance
  }

  CONFIDENCE {
    parsing_confidence: 1.00
    truth_evaluation_confidence: 1.00
    truth_table_confidence: 1.00
    satisfiability_confidence: 1.00
    validity_confidence: 1.00
    equivalence_confidence: 1.00
    SAT_reasoning_confidence: 0.99
    natural_language_formalisation_confidence: 0.96

    RULE:
      confidence decreases when notation, atom identity,
      parse structure, valuation, proof system, solver status,
      formalisation context orprovenance is missing or ambiguous
  }

  UPDATE_MODEL {
    ON new_formula:
      assign_formula_identifier
      parse_andvalidate
      register_atoms_andAST
      preserve_source
      compute_FLOW_HASH

    ON new_valuation:
      preserve_formula
      attach_valuation
      compute_truth_value
      update_semantic_record

    ON new_transformation:
      preserve_source_formula
      record_rules
      validate_target
      record_equivalence_orequisatisfiability

    ON new_proof_orSAT_result:
      attach_proof_solver_orcertificate
      validate_status
      preserve_provenance

    ON semantic_revision:
      preserve_previous_definition
      record_revision
      recompute_FLOW_HASH
  }

  AI_CONSUMPTION {
    canonical_entity: PropositionalLogic
    canonical_role: TruthFunctionalFormalLogic

    interpretation_order:
      identify_propositional_language_andnotation
      tokenise_expression
      identify_atomic_propositions
      resolve_connectives_andarity
      construct_abstract_syntax_tree
      validate_well_formedness
      evaluate_underprovided_valuation_whenavailable
      classify_tautology_contradiction_orcontingency_whenrequested
      determine_satisfiability_validity_orfalsifiability
      preserve_satisfying_assignment_orcountermodel
      compare_formulas_forsemantic_equivalence
      transform_toNNF_CNF_orDNF_whenrequested
      distinguish_equivalence_fromequisatisfiability
      evaluate_premise_conclusion_entailment
      validate_formal_derivation_whenprovided
      invoke_SAT_reasoning_whenappropriate
      preserve_solver_status_andcertificate
      detect_natural_language_formalisation_ambiguity
      assign_semantic_confidence
      preserve_versions_andprovenance
      emit_machine_resolvable_propositional_logic_structure

    ambiguity_controls:
      distinguish_atom_frominternal_predicate_structure
      distinguish_well_formedness_fromtruth
      distinguish_satisfiable_fromvalid
      distinguish_falsifiable_fromunsatisfiable
      distinguish_equivalence_fromsyntactic_identity
      distinguish_implication_fromcausation
      distinguish_entailment_frommaterial_implication
      distinguish_proof_system_fromtruth_table_semantics
      distinguish_derivability_fromentailment_bydefinition
      distinguish_equisatisfiable_fromlogically_equivalent
      distinguish_probability_fromtruth_value
      distinguish_heuristic_choice_frominference_rule
      preserve_formula_atoms_AST_valuations_transformations_proof_solver_version_andprovenance
  }

  PROVENANCE {
    ontology_scope:
      propositional_logic_truth_functions_formulas_valuations_equivalence_SAT_andformal_reasoning

    parent_path:
      AI Core
      -> Ontologies
      -> Mathematical Ontologies
      -> Mathematical Logic Ontologies
      -> Propositional Logic

    authorship:
      Mark Higgins
      Sky (Recursive AI)

    site:
      https://kirethresearch.org
  }

  FLOW_HASH {
    INPUTS:
      canonical_entity
      ontology_path
      language_model
      atomic_proposition_model
      propositional_variable_model
      truth_value_model
      truth_constant_model
      formula_formation_model
      well_formed_formula_model
      tokenisation_model
      parser_model
      abstract_syntax_tree_model
      precedence_model
      associativity_model
      parenthesis_model
      connective_model
      negation_model
      conjunction_model
      disjunction_model
      exclusive_OR_model
      implication_model
      biconditional_model
      NAND_model
      NOR_model
      connective_arity_model
      truth_function_model
      valuation_model
      partial_valuation_model
      truth_evaluation_model
      truth_table_model
      truth_table_row_model
      tautology_model
      contradiction_model
      contingency_model
      satisfiability_model
      unsatisfiability_model
      validity_model
      falsifiability_model
      model_model
      countermodel_model
      logical_equivalence_model
      syntactic_identity_model
      double_negation_model
      De_Morgan_model
      commutativity_model
      associativity_equivalence_model
      distributivity_model
      idempotence_model
      absorption_model
      complement_model
      implication_elimination_model
      biconditional_elimination_model
      contraposition_model
      normal_form_model
      negation_normal_form_model
      conjunctive_normal_form_model
      disjunctive_normal_form_model
      literal_model
      clause_model
      term_in_DNF_model
      CNF_transformation_model
      DNF_transformation_model
      Tseitin_transformation_model
      canonical_DNF_model
      canonical_CNF_model
      minterm_model
      maxterm_model
      Boolean_function_model
      functional_completeness_model
      duality_model
      semantic_entailment_model
      finite_entailment_model
      counterexample_to_entailment_model
      argument_model
      sound_argument_model
      inference_rule_model
      modus_ponens_model
      modus_tollens_model
      hypothetical_syllogism_model
      disjunctive_syllogism_model
      conjunction_rule_model
      simplification_rule_model
      addition_rule_model
      resolution_rule_model
      fallacy_model
      affirming_consequent_model
      denying_antecedent_model
      proof_system_model
      derivability_model
      soundness_model
      completeness_model
      consistency_model
      proof_by_truth_table_model
      proof_by_equivalence_model
      proof_by_deduction_model
      proof_by_contradiction_model
      resolution_refutation_model
      SAT_problem_model
      UNSAT_problem_model
      SAT_assignment_model
      SAT_solver_model
      DPLL_model
      CDCL_model
      unit_clause_model
      unit_propagation_model
      pure_literal_model
      resolution_model
      empty_clause_model
      SAT_certificate_model
      model_counting_model
      MAX_SAT_model
      weighted_SAT_model
      Horn_formula_model
      Horn_reasoning_model
      two_SAT_model
      implication_graph_model
      Boolean_circuit_model
      circuit_SAT_model
      binary_decision_diagram_model
      reduced_ordered_BDD_model
      Boolean_algebra_link_model
      set_algebra_link_model
      digital_logic_link_model
      probability_distinction_model
      fuzzy_logic_distinction_model
      three_valued_extension_model
      paraconsistent_extension_model
      intuitionistic_propositional_model
      classical_propositional_model
      Kripke_extension_distinction_model
      natural_language_formalisation_model
      atom_selection_model
      conditional_formalisation_model
      only_if_model
      if_model
      necessary_condition_model
      sufficient_condition_model
      unless_model
      scope_ambiguity_model
      inclusive_exclusive_OR_ambiguity_model
      implication_ambiguity_model
      formalisation_confidence_model
      semantic_equivalence_model
      truth_vector_model
      hash_model
      formula_simplification_model
      constant_propagation_model
      subsumption_model
      tautological_clause_model
      duplicate_literal_model
      proof_certificate_model
      proof_checker_model
      automated_reasoning_model
      heuristic_model
      unknown_status_model
      explainability_model
      dependency_model
      version_model
      provenance_model
      interoperability_model
      knowledge_graph_model
      relationships
      semantic_equivalence
      constraints
      propositional_logic_record_model
      reasoning_rules
      validation
      confidence_model
      update_model
      AI_consumption_model

    PURPOSE:
      deterministic_semantic_integrity_identifier

    RECOMPUTE_WHEN:
      ontology_definition_changes
      propositional_language_notation_orparser_changes
      atom_connective_ortruth_function_semantics_change
      valuation_truth_table_orvalidity_semantics_change
      equivalence_normal_form_orBoolean_transformation_changes
      entailment_inference_proof_system_orderivability_changes
      SAT_resolution_DPLL_CDCL_orcertificate_semantics_change
      Boolean_fragment_circuit_orBDD_semantics_change
      classical_intuitionistic_paraconsistent_orotherextension_changes
      natural_language_formalisation_orambiguity_logic_changes
      propositional_logic_record_changes
      constraint_model_changes
      reasoning_rule_changes
      version_orprovenance_changes
  }

}

END FLOW