ZTL STUDIO

the table judge what is ZFL?

Check an algebra derivation, step by step

One equation per line, each the next step. Every step is judged by its solution sets, exactly: a step that cancels a factor or divides by an expression can lose a solution, and a step that clears a denominator can gain one where the original was undefined — the witness and the cause are named. Dividing by an expression that is 0 for every value (the "1 = 2" proofs) has nothing to check: E. One unknown; + - * / ^ with whole powers; exact decimals.

Sets defined by a property — self-reference allowed

Give each set as a list of names, as data cell by cell ("T", "F" or "Z" for unknown), or by a property abs of x — which may mention any set, itself included. Every name is also something that can be a member. Membership is decided where the definitions ground it; what they leave undecided gets a passport: PARADOX (no stipulation can repair it), UNDERDETERMINED (consistent, but a decision is owed), INPUT (verify the given cell), DOWNSTREAM (inherits a quarantine). Claims get the judge's dispositions. Formulas: ["in",a,S], ["not",φ], ["and"|"or"|"imp"|"iff",φ,ψ], ["all"|"ex","y",φ], ["eq",S,T].

Both checkers are the ZTL kernel itself (zsteps.py, znaive.py at github.com/inventor1975/ZTL), no AI. A request above the public limits is refused with the reason — run the same files on your own machine for larger ones.