| << Prev | - Up - | Next >> |
In the next chapter, we will discuss the implementation of our propositional tableaux calculus just presented. If you want to use the calculus right away, have a look at our Web-Interface. You can either generate tableaux for some given example formulae or type in formulae yourself (using our familiar Prolog syntax). This might help you doing your exercises.
In the next chapter, we will discuss the implementation of our propositional tableaux calculus just presented. If you want to use the calculus right away, have a look at our Web-Interface. You can either generate tableaux for some given example formulae or type in formulae yourself (using our familiar Prolog syntax). This might help you doing your exercises.
Propositional example formulae like the ones we discussed in this chapter can be found in the choice box Propositional. If you type in examples by hand, don't care about the QDepth input field. Later in the context of first order tableaux, we will learn what this argument is good for.
Try this!
Take for example the tableaux we have seen in Section 7.2.4 and compare it to the tableaux our system generates:
love(mary,bill) & love(john,mary) > love(john,mary) .
Note that you can feed the formula
love(mary,bill) & love(john,mary) > love(john,mary)directly to our system. But of course you can also feed the equivalent formula without defined connectives:
~((love(mary,bill) & love(john,mary)) & ~love(john,mary)).Don't forget to choose whether you want to make the formula true or false.
| << Prev | - Up - | Next >> |