Can I use programming logic to solve logic questions using sentence letters?

[aychamo]

I posted this elsewhere in the forums, but I think this is a much better area for it.

Are there any logic programs to solve logic questions? I mean, the stuff like where you prove an argument valid or invalid with sentence letters.

Like with this (i'm totally making this up, I dont' know if its valid or invalid, just giving an example).

(A v F) > (B*C)
F == C
~Q
----------
F v I

Or whatever, you know what I mean? My logic teacher talked about how a computer could solve them, but was talking about using the 2^X rule to solve it (say 2^6 in this case cause there is 6 different sentence letters.) I have only a shy background in computer science, and I'm curious if you could only solve these types of problems using a huge loop, or if you could solve them by interpretation, and which way would be easier?

Thank you,
AYCHAMO!

 

[Alkatran]

Technicly speaking, a computer can solve any problem you can, if the programmer was intelligent. Computers work on logical comparisons (you can check if two things are equal, you can AND then, OR them.. etc) so I suppose their basis is that...

Think about it this way: It'll solve it after you tell it how, until we get them thinking for themselves.

 

[techwonder]

I think your question was more along the lines if such a program already exists?

I am not an expert, but I remember reading that a program that could perform mathematical deductions had been written and that's several years ago. I also remember though that that program was hailed as a milestone in mathematics and lots of new proofs could be expected "soon". There was even philosophical (and practical) discussions whether "proof by computer" was really proof or not, as they (the proofs) would likely be too long to follow for any human being. Since then I've heard nothing about this. Did anybody? If not then, well, lots of hype and little value ...

 

[MathematicalPhysicist]

i know that there is a software that is built-in the latest mathematica and it is suited for these sort of deductions and inductions problems.

the problem i don't remember its name.

 

[hypnagogue]

I'm positive such programs have been created, although I don't know any specific references offhand.

In any case, it is entirely possible to construct a program that performs logical deductions without the need for constructing truth tables (checking 2^n combinations of truth values for n variables). For instance, given the rule

if A is true and (A => B) is true, then B is true

and the inputs

A is true and (A => B) is true

the computer could deduce that B is true. Likewise for any other logical rule of deduction.

 

[kioria]

Isn't most of the electrical logic gates and XOR mechanisms based on this? I think so.

 

[hypnagogue]

Computer circuits use 2 basic kinds of logical operations, NAND and NOR (the logical inversion of the operators AND and OR respectively). From these 2 operators, any other kind of logical circuit can be created. For instance, NOT A is equivalent to A NAND A, A XOR B is equivalent to (A OR B) AND NOT (A AND B), and the conditional A -> B is equivalent to (NOT A) OR B. (And of course, AND and OR are just NOT NAND and NOT NOR, respectively.)

So there is a sense in which computers solve logic problems all the time. It's what allows them to carry out instructions, do mathematical calculations and so on. In general, though, general logical deductions of the sort asked about by aychamo wouldn't be done with a hardwired set of gates, but rather the logical gates in the processor would carry out a set of higher-level sequences of instructions in order to solve the problem in question. That is, general logic problems with variable numbers of terms and types of operators and the like would require the proper computer program telling the processor what to do with the given input, rather than being built into the basic functioning of the processor itself. If that makes any sense.

 

[MathematicalPhysicist]

here are some proof checkers (not the game (-: )

http://137.99.26.4/~wwwphil/SOFTWARE.HTML
two in the price of one

 

[wave]

I am not an expert, but I remember reading that a program that could perform mathematical deductions had been written and that's several years ago. I also remember though that that program was hailed as a milestone in mathematics and lots of new proofs could be expected "soon".

A computer program can do simple predicate calculus. However, Godel's Incompleteness Theorem proved that it's impossible to create a program for general mathematical proofs.

There was even philosophical (and practical) discussions whether "proof by computer" was really proof or not, as they (the proofs) would likely be too long to follow for any human being.

That's nonsense - nothing personal. I never thought I'd quote the former Prime Minister of Canada, Jean Chretien, but "A proof is a proof. What kind of a proof? It's a proof. A proof is a proof. And when you have a good proof, it's because it's proven."

 

[NeutronStar]

Isetl

You might want to try ISETL (Interactive Set Language)

You can initiate variables like;

p := true; q := false; r := true;

And then ask the program to evaluate statements like:

p and (q or not r);

In this case the program would simply return "false"

It is also programmable so that you can write small programs that will actually change the state of variables based on logic conditions. It has things like "for/do" statements for example.

It will also do basic arithmetic operations on numerical variable like a + b, a * 5, etc. I think it can keep track of limited finite sets and elements too so that you can ask whether something is a member of a set and it will respond with "true" or "false".

I've never actually used this program myself. I took a logic course and our textbook kept referring to this program and had homework problems that made use of ISETL. Unfortunately our instructor didn't have access to computers in our classroom. So we never actually used the program.

By the way, the textbook we used was "Conjecture & Proof" by Diane Driscoll Schwartz ISBN 0-03-098338-X. You might be able to find the book in a library. It's listed on Amazon.com as being out of print which is weird because I just took this course last year!

Anyhow, the ISETL program can be downloaded at the following link for free: (it's available for both Windows and MAC)

http://www.ilstu.edu/~jfcottr/isetl/

Like I say. I never used it, but I think it might be what you are looking for.

Just edited to add that you can get a whole lot more compex than the simple example that I gave above. Like:

((p and not q) or (not p and r)) and ((q or p) and not (p and r));

I'll leave this as an exercise for the readers to evaluate based on my previous assignments for p, q, and r.

You can also have many more variables.

 

[NeutronStar]

Isetlw

I just found this link for an updated version of ISETL called ISETLW for windows:

http://isetlw.muc.edu/isetlw/default.asp