Relations between Logics

• Problem description

• What has been done?

  • The inputs are two logic system files encoded in existing ATP formats. (See Dr. Geoff Sutcliffe's TPTP Encoding)
    • Axioms
    • Rules
    • Operators
    • Example: PCHilbert System
  • The JJParser is used to parse the two inputs and get two lists of axioms .
  • The algorithm 1 to get the relationship between Logics A and Logics B.
  • Expanded form (PCHilbert) is necessary.
    • Why: "Set difference" of two logics doesn't work on conjunctions of "use" atoms
    • Problem:
      • Proving operaters is not necessary
      • It takes more time to prove the "expanded" form file than the "original" form
  • Solutions to using the original file
    • Relabel "axioms" of definition and operator "use" formula to "definition"
    • Split conjunctions of "use" atoms into separate TPTP formulae(Example: PCHilbert system )
    • Make axioms from union of all of "from" system and definition type formulae in "to" system
    • Prove axiom type formulae in "to" system
    • In algorithm 2, neither "subset" nor "set-difference" is necessary.
  • Why should the "relabeling" work?
    • The axioms which previously "subset" and "set-difference" avoided proving in "to" system also appear in "from" system. So, these axioms can be quickly proved.
  • Test result 1.
  • During the testing of "provable" procedure, once the axiom in "to" system gets proved, union it with "from" system to help prove the next axiom; Test result 2.
  • (Modification)During the testing of "provable" procedure:
    <1>For every axiom in "to" system: if an axiom gets proved, add it to the proved list, otherwise add it to the notproved list;
    <2>After every axiom has been tested, if proved list is null, then "to" system can not be proved "provable"; if notproved list is null, then " to" system is "provable"; if neither proved nor notproved list is null, add proved axioms to "from" system, and notproved list is the new "to" system, then go back to <1>;
    <3>Test result 3.
    
  • Add proved axioms to the problem as lemmas:
    • In the proof from S5=KM4B to S5=S1-0M10 add "s1_1, s1_2, s1_3, s1_4, m10, adjunction, modus_ponens_strict_implies" as lemmas to S5=KM4B.sys; No more succeeded.
    • In the proof from S5=S1-0M6S3M9B to S5=KM4B, add "modus_tollens, and_1, and_2, implies_1, or_2, equiv_2, axiom_k, axiom_b" to S5=S1-0M6S3M9B.sys as lemmas; Proved modus_ponens, or_1, equiv_1.
  • The reason why some of the axioms cannot be solved:
    • Mistake in the logic
    • The encoding is too cumbersome
    • Problems are too hard for ATP, like induction which is impossible in ATP
    • Time out

  • What to be done?

    • Add lemmas by hand to unproved problems. (See Table_2)