AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug Donate Contacts

AngouriMath.Functions.Boolean

← Back to list of namespaces

Classes within the AngouriMath.Functions.Boolean namespace

• BooleanSolver

  Summary

  This is set of very simple algorithms
  It's an analogue of Newton Solver as it doesn't represent its answer
  symbolically
  Use
  

• Minimiser

  Summary

  Two-level minimisation of a boolean expression by Quine-McCluskey: the minterms where
  it holds are combined into prime implicants, and a cover is chosen from those.
  

  Remarks

  The rewrite rules reach absorption and nothing past it, so
  a and b or a and not b stopped at a and (b or not b) -- the factoring is
  right and there is no rule to finish it, because b or not b has none reducing it
  to true. One classical algorithm covers that, excluded middle, non-contradiction
  and every larger cover at once, where each would otherwise be its own rule.
  #768

• QuantifierFacts

  Summary

  What the quantifiers around a statement establish while they decide it: each bound name
  is a member of the set it ranges over, and a claim made under a hypothesis is made where
  the hypothesis holds. A rule that needs one of those facts, such as that p is prime
  or that 0 < k < p, asks here.
  

  Remarks

  A node has no parent, so a rule inside a body cannot walk up to the quantifier that binds
  its names. The quantifier hands the facts down instead, for as long as it takes to decide:
  the set its name ranges over, and for forall x in S : H implies C -- or
  C or not H, which says the same -- the conjuncts of H while C is
  simplified. They are never in scope while H itself is simplified, or
  H implies C would lose its hypothesis. For exists and
  exists! each conjunct of the body is simplified with the ones before it in scope.
  Scopes nest, so the inner quantifier of forall p in PP : forall k in ZZ : ... knows
  that p is prime. Nothing leaves a scope: a verdict reached with the facts is the
  verdict on the quantified statement, which states them, and it carries no condition.
  The bound name is renamed first, to a name no other expression has, and every fact is
  about a renamed name. That is what keeps a verdict from escaping through a cache. A node
  that caches its simplification can only have read a fact if it mentions a renamed name,
  and every such node is built during this decision and is reachable from nothing else. A
  cache keyed on the structure of an expression cannot serve it elsewhere either, since no
  other expression has the name. For the same reason a conjunct of the hypothesis about the
  free names alone is not recorded: a rule reading it could simplify a node that is shared.
  A substitution stops at a binder, so an inner quantifier that binds the same name again
  is not renamed through, and the outer facts about the name do not reach it.
  Only a body in which a rule reads the facts is renamed and decided this way. Every other
  statement is decided as it was, under its own names.
  https://github.com/asc-community/AngouriMath/issues/1409
  

• Quantifiers

  Summary

  Decides forall x in S : P, exists x in S : P and exists! x in S : P where a decision is available, and says nothing where it is not.
  

  Remarks

  Three routes, in the order Sullivan and Mackey's proofs book (#1409) teaches them. Over a finite set the body
  is evaluated at every member, which is the definition; a member the body cannot decide
  leaves the statement as written unless the members it can decide settle it, as one
  counterexample settles forall. Over an infinite set the first thing tried is a
  named witness: a handful of members of the set, chosen for being where a claim
  usually fails — 0, ±1, ±2, a half, an end of an interval, i in the complex numbers
  — and a member where the body is false disproves forall exactly as one where it
  is true proves exists. What a witness cannot do is prove forall or refute
  exists, and for that the solver is asked: exists x in S : P holds
  where the solution set of P meets S, and forall x in S : P where the
  solution set of not P does not.
  The solver route is taken only where what it answers is what was asked. Its answer to an
  order comparison is a set of reals, so it is asked one only over a set of reals; its
  default for a statement it has no arm for is the empty set, which as an answer to
  "where does this hold" is a claim, so it is asked only about the shapes it has arms for
  — comparisons of two expressions that mention the variable, joined by the connectives.
  Whether the solution set meets S is read off the two sets by
  Meets(AngouriMath.Entity.Set,AngouriMath.Entity.Set), and where that cannot be read — a set-builder the solver fell back to,
  a member whose membership is undecided — the answer is that there is none.
  Uniqueness is existence with a count: over a finite set of numbers, whose members are
  distinct exactly when unequal; over anything else, from the solver's solution set when it
  is a finite set of numbers. A set with a symbol in it is not counted, since two of its
  members may be one.
  https://github.com/asc-community/AngouriMath/issues/1409