Formula used
Implication uses the equivalence A → B ≡ ¬A ∨ B. Biconditional becomes two implications. Negations move inward using De Morgan rules.
Finite quantifiers expand across every selected domain element. Resolution searches the grounded clause set. Search limits prevent uncontrolled growth.
How to use
- Select a solver mode.
- Enter formulas with symbols or keyboard syntax.
- Declare constants, variables, and a finite domain.
- Provide model JSON for semantic evaluation.
- Submit the form and review every reasoning step.
Accepted notation
| Meaning | Symbol form | Keyboard form |
|---|---|---|
| Negation | ¬P(x) | !P(x) or not P(x) |
| Conjunction | P(x) ∧ Q(x) | P(x) & Q(x) |
| Disjunction | P(x) ∨ Q(x) | P(x) | Q(x) |
| Implication | P(x) → Q(x) | P(x) -> Q(x) |
| Biconditional | P(x) ↔ Q(x) | P(x) <-> Q(x) |
| Universal | ∀x P(x) | forall x P(x) |
| Existential | ∃x P(x) | exists x P(x) |
Example data
| Mode | Input | Expected interpretation |
|---|---|---|
| Entailment | ∀x(Human(x) → Mortal(x)); Human(socrates) | Mortal(socrates) follows in the selected grounding. |
| Unification | Knows(x,father(x)) and Knows(alice,y) | {x ↦ alice, y ↦ father(alice)} |
| Transformation | ¬∀x P(x) | ∃x ¬P(x) |
| Equivalence | ∀x(H(x) → M(x)) and ¬∃x(H(x) ∧ ¬M(x)) | Equivalent in matching finite models. |
Important limitation
General first-order validity is undecidable. A bounded search may stop without finding a proof. That outcome does not establish invalidity.
Finite-model results apply only to the supplied interpretation. Grounded resolution applies only to the selected domain. Review scope notes carefully.
Frequently asked questions
Can this solver decide every first-order formula?
No. General first-order validity is undecidable, so bounded searches may return an unknown result.
Does it support Unicode symbols?
Yes. It accepts common Unicode operators and equivalent keyboard notation.
What is a finite model?
It is a domain with interpretations for constants, predicates, and functions.
How are free variables handled?
Finite-model mode tests every assignment within the selected domain, subject to safety limits.
What does standardised apart mean?
Each bound variable receives a unique name to prevent accidental variable capture.
What does Skolemisation do?
It removes existential quantifiers by introducing fresh constants or functions.
Is the unifier always most general?
The implemented occurs-check algorithm returns a most general unifier for supported first-order terms.
Why can CNF conversion stop?
Distributing disjunctions may grow exponentially, so the calculator enforces a safety limit.
Can I export results?
Yes. You can copy the report, download CSV, or print the page as PDF.