There is a repository of theorem proving problems called Thousands of Problems of Theorem Provers (TPTP.org). This project has the goal of representing the problem in terms of its axiomatic system and conjecture in Wolfram Language, and using the Automated Theorem Proving capabilities of Wolfram Language to build out Proof Graphs of the proof to each conjecture. Using these Proof Graphs will lay the foundations for future analysis of metamathematical properties of the proof space.
Project Details
Project Details
Outline of Project
Outline of Project
Here’s a diagram of the project:
From the project we see that there is essentially 3 main stages:
1) Parsing
2) Building Proof Graph
3) Studying Proof Graphs
1) Parsing
2) Building Proof Graph
3) Studying Proof Graphs
Overview of Selected Problem
Overview of Selected Problem
The Animals Puzzle
[PUZ002-1 : TPTP v9.0.0. Released v1.0.0.]
Link to problem: https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ002-1.p
Axioms:
1) The only animals in this house are cats.
2) Every animal is suitable for a pet, that loves to gaze at the moon.
3) When I detest an animal, I avoid it.
4) No animals are carnivorous, unless they prowl at night.
5) No cat fails to kill mice.
6) No animals ever take to me, except what are in this house.
7) Kangaroos are not suitable for pets.
8) None but carnivora kill mice.
9) I detest animals that do not take to me.
10) Animals that prowl at night always love to gaze at the moon.
Conjecture:
The problem is to prove that “I always avoid a kangaroo”.
[PUZ002-1 : TPTP v9.0.0. Released v1.0.0.]
Link to problem: https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ002-1.p
Axioms:
1) The only animals in this house are cats.
2) Every animal is suitable for a pet, that loves to gaze at the moon.
3) When I detest an animal, I avoid it.
4) No animals are carnivorous, unless they prowl at night.
5) No cat fails to kill mice.
6) No animals ever take to me, except what are in this house.
7) Kangaroos are not suitable for pets.
8) None but carnivora kill mice.
9) I detest animals that do not take to me.
10) Animals that prowl at night always love to gaze at the moon.
Conjecture:
The problem is to prove that “I always avoid a kangaroo”.
Hand Solving the Problem:
(7) Kangaroos are not suitable for pets.
(2) Therefore kangaroos do not love to gaze at the moon.
(10) Therefore kangaroos do not prowl at night.
(4) Therefore kangaroos are not carnivorous.
(8) Therefore kangaroos do not kill mice.
(5) Therefore kangaroos are not cats.
(1) Therefore kangaroos are not in the house.
(6) Therefore kangaroos do not take to me.
(9) Therefore I detest kangaroos.
(3) Therefore I avoid kangaroos. ■
This is useful for trying to understand a proof, but it is not very formal. This is where CNF comes into play.
(7) Kangaroos are not suitable for pets.
(2) Therefore kangaroos do not love to gaze at the moon.
(10) Therefore kangaroos do not prowl at night.
(4) Therefore kangaroos are not carnivorous.
(8) Therefore kangaroos do not kill mice.
(5) Therefore kangaroos are not cats.
(1) Therefore kangaroos are not in the house.
(6) Therefore kangaroos do not take to me.
(9) Therefore I detest kangaroos.
(3) Therefore I avoid kangaroos. ■
This is useful for trying to understand a proof, but it is not very formal. This is where CNF comes into play.
TPTP representation of the problem in Clause Normal Form (CNF)
Parsing Code
Parsing Code
Parsing Problem
Parsing Problem
The general parsing problem is given a string of symbols, how does one convert it into a syntax tree conforming to the grammar rules to understand the structure of the string.
TPTP problems are written in multiple formal logic formulae: monomorphic and polymorphic typed higher-order form (THF), monomorphic and polymorphic typed first-order form (TFF, including the extended first-order form (TXF)), first-order form (FOF), and clause normal form (CNF).
The syntax for how these logic formula are written are described in Backus-Naur Form (BNF). BNF is used as a metasyntax in this context, as it is a syntax used to describe other syntaxes. The full syntax can be found at https://tptp.org/TPTP/SyntaxBNF.html.
So the first part of this project was to build a parser for the TPTP BNF syntax.
TPTP problems are written in multiple formal logic formulae: monomorphic and polymorphic typed higher-order form (THF), monomorphic and polymorphic typed first-order form (TFF, including the extended first-order form (TXF)), first-order form (FOF), and clause normal form (CNF).
The syntax for how these logic formula are written are described in Backus-Naur Form (BNF). BNF is used as a metasyntax in this context, as it is a syntax used to describe other syntaxes. The full syntax can be found at https://tptp.org/TPTP/SyntaxBNF.html.
So the first part of this project was to build a parser for the TPTP BNF syntax.
The Code
The Code
This code was run locally in a Python virtual environment using External Evaluate. I used a package called tptp-lark-parser that is a package that uses the Lark Python Parser to build a parser for CNF formed TPTP problems (unfortunately only works for CNF and none of the other logic formula). The Github to this package: https://github.com/inpefess/tptp-lark-parser.
In[]:=
code=;pythonPath="/usr/local/bin/python3"session=StartExternalSession[<|"System"->"Python","Evaluator"->pythonPath|>];ExternalEvaluate[session,code]
Out[]=
/usr/local/bin/python3
“code” and Outputs are iconized for space. The “code” variable is just a string of Python code with the TPTP Problem in CNF that is being parsed. The Outputs are the TPTP parsed problem and the parsed problem turned into JSON using jsonpickle.
If one would like to see the code in a more readable Python format, one can run ToString[code]. I have ran it in this notebook, so clicking on the cell at the right should open the output:
If one would like to see the code in a more readable Python format, one can run ToString[code]. I have ran it in this notebook, so clicking on the cell at the right should open the output:
In[]:=
ToString[code]
The JSON data is also an output, however the JSON data in the code is saved to a file. I use an Import function to call it. One can can also open the JSON data in the same manner:
In[]:=
importedJsonData2=Import["/Users/arihantgadgade/Documents/Academic/Wolfram Physics/WSS2024/TPTP_Project/TPTPlarkparser/parsed_object3.json","RawJSON"]
Functional Parsers Side Note
Functional Parsers Side Note
Initially I tried to build the TPTP parser using a Wolfram Language Functional Parsers Paclet (created by Anton Antonov), however this proved quite difficult and due to time constraints I moved to a Python parser.
However creating a Wolfram Language parser is certainly feasible, and will offer several benefits.
1) Will allow everything to be within one framework, so more users can play with the proof objects.
2) This will also allow for parsing all the problems in TPTP, as the tptp-lark-parser is restricted to only CNF problems.
3) Will allow for an easier time turning the parsed problems into associations/rules for the Automated Theorem Proving capabilities in WL.
However creating a Wolfram Language parser is certainly feasible, and will offer several benefits.
1) Will allow everything to be within one framework, so more users can play with the proof objects.
2) This will also allow for parsing all the problems in TPTP, as the tptp-lark-parser is restricted to only CNF problems.
3) Will allow for an easier time turning the parsed problems into associations/rules for the Automated Theorem Proving capabilities in WL.
That will essentially turn the project diagram to look like this:
Representing Proof Problems as Axiomatic Systems
Representing Proof Problems as Axiomatic Systems
So after using a parser to parse a problem, and creating the JSON association of the problem, one must represent the JSON association into an association of the axioms and conjecture that FindEquationalProof is able to use.
Here’s the Association of the Animals Puzzle from the parsed problem:
Here’s the Association of the Animals Puzzle written from scratch that follows the structure above, but is more human interpretable (makes it easier to read the proof graph):
Side Note: Due to time constraints I wasn’t able to build out a method for converting from JSON to the Axiom Association. I will build this in the future.
Creating Proof Graphs
Creating Proof Graphs
Proof graph from the Association of the Animals Puzzle from the parsed problem:
Proof Graph of the Association of the Animals Puzzle written from scratch:
Analysing Proof Graph
Analysing Proof Graph
Here are the two graphs side by side:
We see that it has similar structure, but not exactly the same. I am currently unsure why this occurred, further analysis into the mechanism of the Automated Theorem Prover may be required.
Using the Options defined in the documentation for ProofObject is a good way to get an idea of the structure of the proof.
Potential Future Analysis:
1) I can build a multiway system with multiple ProofObjects using the same axiomatic system. This would allow for doing metamathematical analysis for the Proof Problem.
2) Using different axiomatic systems that prove the same conjecture and analysing the Proof Objects.
The goal is to analyze the space of all possible proofs and any methodologies to achieve that are the path.
1) I can build a multiway system with multiple ProofObjects using the same axiomatic system. This would allow for doing metamathematical analysis for the Proof Problem.
2) Using different axiomatic systems that prove the same conjecture and analysing the Proof Objects.
The goal is to analyze the space of all possible proofs and any methodologies to achieve that are the path.
Concluding Remarks
Concluding Remarks
Still quite a bit I can do with this project:
1) Build out the TPTP Functional Parser in WL.
2) Build ProofGraphs for all the rest of the TPTP problems.
3) Analyze the structure of all the ProofGraphs and begin building multiway systems.
1) Build out the TPTP Functional Parser in WL.
2) Build ProofGraphs for all the rest of the TPTP problems.
3) Analyze the structure of all the ProofGraphs and begin building multiway systems.
Acknowledgments
Acknowledgments
Nikolay Murzin (Mentor)
Hatem Elshatlawy (Mentor)
Anton Antonov: Generously offered time and help for understanding and using his Functional Parser paclet.
Hatem Elshatlawy (Mentor)
Anton Antonov: Generously offered time and help for understanding and using his Functional Parser paclet.
Extend my special thanks to Stephen Wolfram for suggesting this project.
Access the Full Code
Access the Full Code
Cite This Notebook
Cite This Notebook