Representation, Verification, and Visualization of
Tarskian Interpretations for Typed First-order Logic
Abstract
This talk describes a new format for representing Tarskian-style
interpretations for formulae in typed first-order logic, using the TPTP
TF0 language.
It further describes a technique and an implemented tool for verifying models
using this representation, and a tool for visualizing interpretations.
The research contributes to the advancement of automated reasoning technology
for model finding, which has several applications, including verification.