Tabs & Files

• Click a tab to switch between open files.
• Double-click a tab to rename the file.
• Drag a tab left/right to reorder tabs.
• Click the x on a tab to close it.
• A small dot after the name means the tab has unsaved changes.

File menu

• File -> New: create a new empty file of the chosen type (KIF, TQ, TPTP, THF, TFF, FOF, CNF).
• File -> Open File: open a file previously saved in your user area.
• File -> Save: save the current tab to your user directory (overwrites if the name already exists).
• File -> Save As: save the current content under a new name.
• File -> Download: download the current buffer as a plain text file.
• File -> Upload: load a file from your local machine into a new tab.

Automated Theorem Proving

• Open a TQ or TPTP-family tab and select ATP in the header.
• Choose an installed prover and its options, then run the query or problem file.
• The TQ meta-predicates determine whether FOF, TFF, or THF translation is used.
• TPTP, P, FOF, TFF, THF, and CNF buffers are complete problem files. They are passed directly to the prover, including any conjectures already in the file.

Editing & Formatting

• The editor automatically chooses syntax highlighting based on the file extension (.kif vs .tptp/.thf/.tff/.fof/.cnf).
• Use the Format button in the header to pretty-print the current buffer (KIF or TPTP).
• After you stop typing for about 2 seconds, the editor automatically runs checks.
• Errors and warnings appear in the right-hand panel and are highlighted in the gutter and text.

Checks & Errors

• Red lines / text indicate errors; yellow indicates warnings.
• Each error shows file, line, and column, plus a message.
• If the buffer is empty, the checker does nothing.