KGKherian Gracher
PTEN
Menu

Ideas in practice

Logic Lab

Tools I develop to support teaching and research in Philosophy and Logic.

66 logical profiles

Logic
Trees

A comprehensive tableaux laboratory for exploring classical and non-classical systems.

Open the Tableaux Laboratory (Portuguese) Public access · no account required.

One logic is not all logics.

  • Broad catalogue. 66 profiles spanning classical, paraconsistent, intuitionistic, modal, temporal, conditional and description logics.
  • Visual construction. Enter formulas, follow their tree decomposition and consult the tableau method appropriate to each profile.
  • Learning context. Each logic has a guide covering its origins, authors, significance, innovations, applications and essential bibliography.

From classical logic to the KG Systems. The laboratory includes first-order logic, many-valued families, the da Costa hierarchy, KG Systems, the modal cube, LTL, CTL, PDL and other established calculi.

The specialized KG Systems calculator remains in the Research section; this application provides a broad, comparative view.

Classical propositional deduction

Natural
Deduction

Build proofs in Fitch notation, with subproofs and formal verification.

Open Natural Deduction Public access · no account required.

Your argument, step by step.

Free and assisted modes in the same interface. You choose the rules and references; the engine checks each step and its scope.

Copy your proof as Unicode, Markdown, HTML or LaTeX/Fitch. Computation runs locally; proofs are not stored.

Classical propositional logic

Truth
Tables

Explore every valuation of a formula, from its variables to the result.

Open Truth Tables Public access · no account required.

One formula, every possibility.

Identify tautologies, contradictions and contingencies. Follow the subformulas and copy the table as LaTeX, Markdown, HTML or text.

Local computation; formulas and results are not stored.

Classical propositional logic

Formal
Analysis

Check validity, satisfiability, logical equivalence and argument validity.

Open Formal Analysis Public access · no account required.

Results and counterexamples.

Inspect valuations that satisfy a formula or show why a formula is not valid, two formulas are not equivalent, or an argument is invalid.

The same engine as Truth Tables, with no AI and no stored work.

Formal engines

Logical Systems
Comparator

Compare the validity of a formula across the computationally available systems.

Open Comparator Public access · no account required.

A result with an explicit procedure.

Inspect the method used and the available open branches or countervaluations. Undetermined results, incompatible languages and errors are identified separately.

No ranking of systems, AI or stored queries.