José A. AlonsoLecturas compartidas el 11 de junio de 2024. https://jaalonso.github.io/vestigium/posts/2024/06/12-lecturas_compartidas_el_11-jun-24 #ITP #Lean4 #IsabelleHOL #Math #ATP #TPTP #FunctionalProgramming #Haskell #Ocaml
The new TPTP format for interpretations. ~ Geoff Sutcliffe, Alexander Steen, Pascal Fontaine. https://arxiv.org/abs/2406.06108 #ATP #TPTP
The New TPTP Format for Interpretations
This paper describes the new TPTP format for representing interpretations. It provides a background survey that helped us ensure that the representation format is adequate for different types of interpretations: Tarskian, Herbrand, and Kripke interpretations. The needs of applications that use models are considered. The syntax and semantics of the new format is expounded in detail, with multiple examples. Verification of models is discussed. Some tools that support processing the new format are noted. The properties of interpretations represented in the new format are discussed.
Lecturas compartidas el 30 de mayo de 2024. https://jaalonso.github.io/vestigium/posts/2024/05/31-lecturas_compartidas_el_30-may-24 #ITP #Lean4 #IsabelleHOL #Coq #Theorema #HOL_Light #Math #ATP #Prover9 #Vampire #TPTP #FunctionalProgramming #Haskell #LogicProgramming #Prolog #AI #LLMs
Automated theorem proving for Prolog verification. ~ Fred Mesnard, Thierry Marianne and Etienne Payet. https://ww.easychair.org/publications/download/n9Jl #ATP #Vampire #TPTP #Prolog