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.