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 Apri, 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.