Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic.

This paper 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 au- tomated reasoning technology for model finding, which has several applications, including verification.