Skip to content

Hold excluded middle whichever operand carries the negation (#876) #877

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Rafael-SOWNet merged 1 commit into from
Aug 11, 2026
Merged

Hold excluded middle whichever operand carries the negation (#876) #877

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions Sources/AngouriMath/Functions/Simplification/Patterns/Patterns.Boolean.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,9 @@ private static bool IsLogic(Entity a, Entity b, Entity c)
Andf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 | any2),
Orf(Notf(var any1), Notf(var any2)) when IsLogic(any1, any2) => !(any1 & any2),
Orf(Notf(var any1), var any1a) when any1 == any1a && IsLogic(any1) => True,
// The same law with the operands the other way round. `or` is commutative, so
// leaving this out made the answer depend on which side the negation was written.
Orf(var any1a, Notf(var any1)) when any1 == any1a && IsLogic(any1) => True,
Orf(Notf(var any1), var any2) when IsLogic(any1, any2) => any1.Implies(any2),
Andf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
Orf(var any1, var any1a) when any1 == any1a && IsLogic(any1) => any1,
Expand Down
23 changes: 23 additions & 0 deletions Sources/Tests/UnitTests/Common/SimplificationRegressionTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -434,5 +434,28 @@ public void ExpandKeepsTheValueOfAQuotientOfFactorials(string input, int at, dou
[InlineData("(x + y + 1)! / (x + y)!")]
public void ExpandCancelsAQuotientOfFactorialsRatherThanLeavingIt(string input)
=> Assert.DoesNotContain(input.ToEntity().Expand().Nodes, node => node is Entity.Factorialf);

// https://github.com/asc-community/AngouriMath/issues/876
// There was one excluded-middle rule and it matched the negation on the left operand
// only. `or` is commutative, so the same proposition had two answers depending on
// which side it was written: `not (x < 0) or (x < 0)` was True while
// `(x < 0) or not (x < 0)` was left as written. A bare variable hid it, because the
// boolean minimiser reduces those whichever way round they are — it takes a
// comparison, which the minimiser does not treat as an atom, to see it.
[Theory]
[InlineData("not (x < 0) or (x < 0)")]
[InlineData("(x < 0) or not (x < 0)")]
[InlineData("not (x > 0) or (x > 0)")]
[InlineData("(x > 0) or not (x > 0)")]
[InlineData("not (x <= 0) or (x <= 0)")]
[InlineData("(x <= 0) or not (x <= 0)")]
[InlineData("not (a = b) or (a = b)")]
[InlineData("(a = b) or not (a = b)")]
[InlineData("not (x in RR) or (x in RR)")]
[InlineData("(x in RR) or not (x in RR)")]
[InlineData("not p or p")]
[InlineData("p or not p")]
public void ExcludedMiddleHoldsWhicheverOperandCarriesTheNegation(string input)
=> Assert.Equal(Entity.Boolean.True, input.ToEntity().Simplify());
}
}
Loading