TPTP Editor

TPTP Editor is a Visual Studio Code extension that provides a streamlined development environment for working with the TPTP language — a standard format used extensively in automated theorem proving and formal logic research.

Built by Daniel Li in collaboration with Dr. Geoff Sutcliffe, the creator of the TPTP library, the extension features full syntax highlighting for both CNF, FOF, THF, etc. formats, enabling clear visual structuring of axioms, hypotheses, and conjectures. It recognizes '.p' & '.s' problem files, supports pretty-printing and safe character escaping, and integrates directly with the SystemOnTPTP + SystemOnTSTP service, allowing users to author, submit, and view solver results without leaving the editor.

Designed for researchers, students, and logic developers. TPTP Editor enhances productivity and readability in formal logic workflows within the comfort of VS Code.

Features

- TPTP Language Features

• Syntax highlighting for .p and .s files
• Support for:
  • Single-line % commentsw
  • Block comments /* ... */
  • Quoted strings
  • Logical operators and quantifiers
  • $-prefixed system constants
  • TPTP directives like fof, cnf, thf, etc.
  • Various special characters (~, |, &, etc.)
• Clean and consistent token coloring across themes
• Real-time error diagnostics and checking

TPTP Extension Functionality

• Pretty-prints TPTP problem content inside the webview for readability
• Custom file icons for '.p' & '.s' files inside VS Code
• Automatically parses and extracts content for submission to theorem provers
• Import problems and solutions directly from the TPTP library
• Provides download support for solution outputs directly from the Webview
• Enables side-by-side comparison of problems and their solutions in VS Code
• Supports multiple TPTP problem domains and systems

Theorem Proving & Solution Processing

• Seamless integration with the SystemOnTPTP & SystemOnTSTP services for remote automated proving
• Supports selection from dozens of available theorem provers (e.g. E, Vampire, CVC5, iProver, Z3, etc.)
• Allows users to choose between TPTP format and native system output for flexibility in results
• Displays the raw and formatted problem & solution returned from the prover inside a dedicated Webview
• All syntax highlighting, Webview styling, and UI accents automatically adjust to the active VS Code color theme, ensuring visual consistency and accessibility across light, dark, and high-contrast themes.

• TPTP: Prove Problem
• Submit the currently open TPTP problem file to a selected theorem prover for evaluation and view results in a rich Webview interface.

• TPTP: Prove Problem Using Multiple Provers
• Run the problem against multiple supported provers simultaneously (e.g. Vampire, E, CVC5) to compare solver behaviors, timings, and proof outputs side-by-side.

• TPTP: Process Solution
• Extract and format a single selected solution for the current problem, with support for downloading or viewing clean, readable output directly in the editor.

• TPTP: Process Solution Using Multiple Processors
• Automatically collect and process all available solution variants for a problem from SystemOnTPTP, allowing users to review results across different systems.

Requirements

No dependencies required — just install and start editing .p or .s files.

Extension Settings

This extension does not contribute any custom settings.

Release Notes

See Release Notes here.

For TPTP Language

The Thousands of Problems for Theorem Provers (TPTP) World is the established infrastructure used by the Automated Theorem Proving (ATP) community for research, development, and deployment of ATP systems. The TPTP format is widely used in logic and automated reasoning. Learn more at http://www.tptp.org

Development Notes

• Grammar implemented via a tmLanguage.json file
• Uses TextMate scopes compatible with popular VS Code themes
• Lexer/grammar derived from an existing BNF TPTP grammar
• Actively tested against a large sample of problems from the official TPTP problem library
• Webview-based prover runner panel implemented with custom form UI to prove theorems

Enjoy using TPTP Editor!