Enter Logic Model and Formula
The calculator checks first-order logic over a finite domain. It supports predicates of any arity, constants, equality, quantifiers, and common connectives.
Example Data Table
| Scenario | Domain | Constants | Predicates | Formula | Expected result |
|---|---|---|---|---|---|
| Every human has a child | alice, bob, carol | a = alice; b = bob | Human/1 = alice | bob | carol Parent/2 = alice,bob | bob,carol | forall x (Human(x) implies exists y Parent(x,y)) | False |
| Someone knows everyone | alice, bob, carol | a = alice | Knows/2 = alice,bob | alice,carol | alice,alice | bob,bob | exists x forall y Knows(x,y) | True |
| Free variable search | 1, 2, 3 | c = 2 | Less/2 = 1,2 | 1,3 | 2,3 | Less(x,c) | Satisfiable |
Formula Used
This calculator uses finite-model semantics for first-order logic. An atomic predicate is true when its evaluated tuple appears in the predicate relation table. Equality is true when both evaluated terms name the same domain element.
Negation flips the truth value. Conjunction returns true only when both subformulas are true. Disjunction returns true when either subformula is true. Implication is false only when the left side is true and the right side is false. Biconditional is true when both sides share the same truth value.
Universal quantification checks every domain element for the bound variable. Existential quantification checks whether at least one domain element makes the subformula true. When a formula has free variables, the calculator evaluates many assignments and reports satisfiability, witnesses, and counterexamples.
How to Use This Calculator
- Enter a finite domain, using commas or new lines.
- Map any constants to existing domain values.
- Define predicates with arity and tuples, such as
Parent/2 = alice,bob | bob,carol. - Type your logical formula using keywords like
forall,exists,and, andimplies. - Click Solve Formula to view the truth value, parsed formula, valuation table, and evaluation trace.
- Use the CSV and PDF buttons to export the computed summary and valuation results.
Frequently Asked Questions
1. What does this solver actually compute?
It evaluates first-order logic formulas over the finite domain you provide. It checks predicate tuples, constants, equality, quantifiers, and connectives, then reports whether the formula is true, satisfiable, or unsupported by the current model.
2. Does it prove formulas in every possible model?
No. It performs finite model checking for the specific domain and relations you enter. A formula may be true here but false in another interpretation with different domain elements or predicate relations.
3. Can I use free variables without quantifiers?
Yes. The calculator builds a valuation table for the free variables and tests many assignments. That helps you locate witnesses, counterexamples, and the combinations that satisfy the open formula.
4. How should I enter predicates?
Use one definition per line with arity and tuple data. Example: Parent/2 = alice,bob | bob,carol. Unary predicates can use single values, such as Human/1 = alice | bob.
5. Which operators are supported?
You can use forall, exists, not, and, or, implies, iff, parentheses, and equality. Symbol versions like ∀, ∃, ¬, ∧, ∨, →, and ↔ are also accepted.
6. Why do I get an unknown term error?
That happens when a symbol is not bound by a quantifier, not defined as a constant, and not present directly as a domain element. Add it to the model or bind it inside the formula.
7. What is the assignment limit for?
Open formulas can create many variable combinations. The assignment limit prevents huge tables and slow pages. Increase it when you need broader testing, but remember that large domains grow quickly.
8. What are the best uses for this tool?
It is useful for teaching semantics, checking homework examples, validating small logical models, exploring witnesses and counterexamples, and debugging finite relational structures before moving to larger proof systems.