Revision history [back]

I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which="" is="" a="" contradiction.<="" p="">

Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, i="" add="" an="" edge="" a-="">b to the graph. If the graph has a directed cyclic (e.g. a->b->c->a), this is a contradiction.

Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and="" "e<a",="" this="" is="" a="" contradiction.<="" p="">

What is a good way to implement this?

I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which="" is="" a="" contradiction.<="" p=""> which is a contradiction.

Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, i="" add="" an="" edge="" a-="">b I add an edge a&rarrow;b to the graph. If the graph has a directed cyclic (e.g. a->b->c->a), a→b→c→a), this is a contradiction.

Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and="" "e<a",="" this="" is="" a="" contradiction.<="" p=""> and "e<a", this is a contradiction.

What is a good way to implement this?

I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which is a contradiction.

Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, I add an edge a&rarrow;b a→b to the graph. If the graph has a directed cyclic (e.g. a→b→c→a), this is a contradiction.

Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and "e<a", this is a contradiction.

What is a good way to implement this?

I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which is a contradiction.

Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, I add an edge a→b to the graph. Then, I check "digraph.all_simple_cycles()". If it is not empty, i.e. the graph has a directed cyclic (e.g. a→b→c→a), cycle such as a→b→c→a, this is a contradiction.

Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and "e<a", this is a contradiction.

What is a good way to implement this?

I am working on a theorem prover related to inequalities. It works in the following way: it assumes, by contradiction, that certain inequalities are true. Then, it proves that there is a cyclic inequality, such as: a<b<c<a, which is a contradiction.

Initially I did this with a poset. Then, thanks to Nathann, I switched to using a DiGraph. For each inequality a<b, I add an edge a→b to the graph. Then, I check "digraph.all_simple_cycles()". If it is not empty, i.e. the graph has a directed cycle such as a→b→c→a, this is a contradiction.

Now, I want to add equalities. I want to be able to add a fact such as "d==e". Then, if the graph contains the inequalities "a<d" and "e<a", this is a contradiction.

What is a good way to implement this?