Reports

Links to recorded lectures: Overview, Practicum PRP,FOF, Practicum FOF,TFF, Principles, Practicum TXF,THF,NTF.

Met Andres Caicedo, who has joined the StarExec development team.

Worked on a design for using LLMs to answer questions from SUMO documentation, and check the answers using the corresponding SUMO logic using the TPTP World.

Helped with the research projects of Richard Thompson (PhD) and Jack Timberlake. (MS).

Worked with Adam to debug the TFF export of SUMO, which prompted the addition of AddTypes and Leo-III-STC to SystemB4TPTP.

Led a Computer Science faculty "brainstorming" session, which ended up delving into trust of AI systems. Useful ideas about "expectations".

Met Peter Denning, and had in interesting conversation about AI systems. Read some of his papers.

Understood and explained to Adam how naive export of modalities from SUMO to TFF could lead to modal collapse.

Taught 16 classes of CS4921, on logic and ATP in the TPTP World, to ten graduate students (officers in the Navy).

Introduced to Valeria De Paiva - a useful contact in the math/logic world.

Seminar on 24th, tutorial session on 25th. Definite interest from the undergrad students.

Met Frabizio, who will provide some AMT2 problems for me to convert to TPTP, try solve, and add to the TPTP.

Encoded a resource conflict problem for Daniel. He will provide larger exampls networks, I will revive MANSEX to extract all conflicts.

Upgraded KSP to use SZS reporting in output.

Devised TPTP format for KSP proofs.

Extended GDV to verify KSP proof with modal connectives.

Started on work to make KSP read TPTP format problems.

Seminar on 10th, tutorial session on 13th. Some really smart undergrads and newly startinging PhD students.

Worked with Haniel to understand Alethe proofs. Converted some Alethe proofs to TSTP format by hand, as a proof-of-concept.

Disvcussed possibility of TSTP format export from Carcara.

Met Mallku Soldevila, discussed Alethe proofs in the Eunoia context.

Seminar and tutorial on 20th. Morning and half the afternoon. A few very keen students in the afternoon, covered some of the principles of ATP.

Worked with Sasha to plan translation of PDDL planning problems to TPTP format.

Seminar on 24th.  Very bright students.

Email from two students asking for my papers.

Discussed translation for Althe format to TSTP format with Peter Baumgartner. He started coding an extension to his SMT2TPTP tool.

Learned about Peter's Fusemate system for probabilistic reasoning. Converted an example to a TPTP-style format for his consideration.

Discussed Peter's calculus for goal-directed reasoning with normalisation by rewriting. I suggested an improvement that allows ordering of the chosen parent. Her doesn't seem to like it :-).

Seminar on 27th, tutorial on 28th (only 1 hour, so no time for students to practice). Tutorial included some people from YesLogic.

Agreed with Cezary to extend the TPTP World to include dependent types. Cezary had done all the work: the syntax is already sufficient, he and his student Daniel Ranalter have a collection of 169 problems. I got the version of Cezary's Lash system that can do type checking for problems with dependent types, and initial testing suggests there is some work to be done on Lash and the problems. This version can also do proving for these problems.

Met Sebastian Sardina and Nir Lipovetzky, who work on planning. The connection was made by Sasha Rubin from the U Sydney visit. I showed them my encoding of the event calculus, and they said for planning I don't need all that and should use the simpler situation calculus. They showed me examples in PDDL, to be converted to TFF.

Seminar on 1st April. Small audience, some there out of politeness :-). 5? students.

Good meetings after the seminar with Tim French (psychology of AI, ethics - got some good reading) and Matthew Daggit (verification of ML - got sources for SMT2 problems, quantum computing, idea to use sentiment analysis for evaluating ethical data points). 

Seminar on 3rd April. Reasonable audience, but I was not on top form. Interesting questions from David Suter. Two students talked to me afterwards about the TPTP World.

Seminar on 7th April. Audience was familiar with the general topic, and lapped it up.

Excellent conversation with Ichiro afterwards, during which he explained his main projects. I gave him the idea to feedback from the formal specification to the user in natural language. He understand that we might be able to collaborate in the future.

Seminar on 10th April, four hours of tutorial on 11th. Active and intereted audince at the seminar, 8 people in the tutorial. Active and inquisitive audience.

Learned a lot about rewriting systems. Teppei sent some "hard" UEQ problems, some of which I could solve with the latest Vampire that I have - I sent the binary to him. Used IDV to summarize a Vampire proof of a problem, and then extract lemma to identify the step that Toma could not do - a useful way to focus in on w place for possible improvement.

No seminar or tutorial due to Easter break

Meeting with Jun Liu on 22nd, discussing S-CS family of ATP systems.  We also tried ChatGPT for converting Jun's PwC contract example to TPTP TFF format - amazingly good. Read papers from Chengdu authors.

Worked on English to TPTP TFF translation.

Zoom meeting with Jun and Chengdu group on 23rd. Good presentations from Chengdu people which gave me a fuller understanding of their triangle method. Read more papers, realized there is a link to Model Elimination.

Dinner with Hui Wang from Queens University on 24th. Gained understanding of the projects with PwC.

Dinner with Chris Nugent (head of CSC@UU) on 25th. Gave him an overview of what Jun and I are working on.

Another meeting with Chengdu group on 28th, in which I presented my observations regarding Model Elimination and integration of equality reasoning in the S-CS systems.

Meeting with UM student Danial Haroon on 28th - he will implement an English to TPTP TFF translator.

Project meeting with Chris Nugent on 28th. Arranged to get sample Smart Home LTL logic to translate to logic.

Productve meeting with Korovin in the morning of 30th, leading to suggestions about proof formats, ideas about the ProoVer competition, decision to retain CASKet in IJCAR years, and changes to the CASC-30 ICU design.

Seminar on 30th to a small but attentive audience. Good questions from one of the postdocs, who continued the conversation after the seminar.

Minimal attendance at the tutorial on 1st May, which instead became a constructive demonstration and discussion of the TPTP World tools. Some software rot was revealed. Great questions from an undergrad student in the session.

Worked with Korovin to containerise iProver, but no success. I made a contact with a wizard at ENS Paris-Saclay, which will hopefully get the containerization completed.

Discussion in the evening about an interesting inference system, its soundness, completeness, and pragmatic usefulness.

Productive meeting with Sean and his PhD student Mantas Baksys in the afternoon of 6th, leading to agreement on the principles of my proposed TPTP format for tableau. Also a wonderful tour of Trinity College (chapel, library, etc.)

Another meeting in the morning of 7th, finalizing the "lemma" rule, and agreeing to submit a paper to the Weidenbach'60 workshop.

Seminar on 7th to an audience of about 30. All apparently knew plenty about logic and reasoning, which made the talk easy to give with the opportunity to address slightly more advanced topics. Good questions at the end. Emails from two of them asking for papers. I think some of them will provide feedback on the DTF proposal (developed at U Melbourne earlier on the tour).

Good chat with Mateja Jamnik after the talk, with an exchange of some papers. She suggested I attend tyhe BigProofs workshop at U. Cambridge in June, but it conflicts with my ENS Paris-Saclay visit. 

Meeting with Abhishek on the 9th, during which he explained his technique for proving properties of regular expressions, for which induction is required. I suggested using it for some simple list properties that require induction.

Seminar on 9th to the Theory group. Good audience of about 20. All apparently knew plenty about logic and reasoning, which made the talk easy to give with the opportunity to address slightly more advanced topics. Good questions at the end.

Meeting with Abhishek and Mirco Giacobbe about verification of neural nets. Looking for ways I can contribute to the final step in the verification chain. 

Seminar on 12th to the group. Knowledgeable audience of about 12. All knew plenty about logic and reasoning, which made the talk easy to give. Lots of questions about interaction with LLMs.

Meetings with Nikolaj on the 12th, implemented an MCP server for SystemOnTPTP. Worked out how to use Z3 to translate TPTP syntax to SMT2.

Meeting with Nikolaj on 13th, upgraded Z3 on SystemOnTPTP to 4.15.1 (including an increase in token length in the parser that I requested to solve Pulina's problems for verification of neural nets).