View Single Post
  #1   Report Post  
Posted to microsoft.public.excel.worksheet.functions
socrates socrates is offline
external usenet poster
 
Posts: 1
Default how to build a "theorem prover" in Excel

My objective is to teach formal logic (some theorems of propositional logic)
to people who may know the Excel basic functions and have some knowledge of
logic.

My idea is to use a very simple true table, so I can give it in a beginners
class.

Example : I want to prove the formula : (A^ B) - B

1st STEP (done!)
column A is associated to the function "A", in Excel
column B is associated to the function "B", in Excel
columns A, B., have the logic values of A and B
column C has the formula to prove

TABLE
A B (A^ B ) - B
1 0 0 = OR ((A*B) <= B) +0
2 1 0 = OR ((A*B) <= B) +0
3 0 1 = OR ((A*B) <= B) +0
4 1 1 = OR ((A*B) <= B) +0

result
A B (A^ B ) - B
1 0 0 1
2 1 0 1
3 0 1 1
4 1 1 1

So the given formula is true for all the values of A and B.

2nd STEP
It is given the formula (A^ B) - B written in cell C1,
and the true table must verify it automatically.
I tried the text functions, but it does not work

A B C
1 (A*B ) =< B
2 0 0 = ?
3 1 0 = ?
4 0 1 = ?
5 1 1 = ?

expected result
A B C
1 (A*B ) =< B
2 0 0 1
3 1 0 1
4 0 1 1
5 1 1 1

Any ideas ?

sorry for my English

Regards
Alvaro