Skip to content

support for inequations and deductions #23

Description

@lzace817

when we do basic algebra, we want to use rules of equivalence:

  • = in math;
  • if and only if in logic;
  • equivalence relation in abstract algebra.

and this is what we have in noq.

but sometimes we need thing that have some sort of order:

  • < in math;
  • imply in logic;
  • partial order in abstract algebra.

the killer application for this, is the ability to make logical deductions.

you can deduce Q from P and Q .
but you can not deduce P and Q from Q.

so we would have rules like:
A ^ B -> A
that allow us to replace the lhs by rhs. And also rules like:
A^B == B^A
that works both ways.

I suppose the way shaping would work in 2 possible ways:

  • manual mode where a shaping operation can be selected to be either equivalece of deductive (noob)
  • auto mode where shaping would be internally deductive, but if all steps are equivalence,
    the result must be equal. (pro)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions