Logical methods for AI

Tools

Tools for syntax, models, normal forms, automated reasoning, proofs, and circuits.

Enter your own formulas, models, and proofs, or check work you did by hand. The tools are grouped by task. Resolution, natural deduction, and Lean each bring their propositional and first-order versions together on one page.

Each page states its supported language and inputs and links to the relevant chapter explanations.

The apps run in your browser. Saved workspaces are files on your device. The Lean translator sends code to the external playground only when you follow its “Open in Lean” link.