Help on Server-side Tasks

The advantage of server-side processing is that you can use any browser of your choice, even if it does not support Java or even graphics. Furthermore the amount of data that needs to be transmitted is relatively small, and your computer does not need to process any calculation. The disadvantage is that you need an online connection to the Internet while using server-side functions.

Currently, there are the following server-side functions:

• detailed truth table - the server shows the truth table of the proposition entered. This truth table contains a column for each connective. The column representing the main connective of the sentence is marked by asterisks.
• truth table (results only) - the server shows the truth table of the whole proposition entered
• Quine-McCluskey optimization - the proposition is optimized using Quine/McCluskey's method.
• Intuitionistic validity - the server checks if the proposition is valid intuitionistically. Note that this task does not support biconditionals.
• Tautology check - the server checks if the proposition is a tautology, i.e. if it is true in every possible world.
• Graphical expression tree - The server graphically shows the syntactical structure of the proposition entered. This task requires your browser to be able to display graphics.
• Graphical alpha tree - The server shows an Alpha Graph representing the proposition entered. This task requires your browser to be able to display graphics.
  A few remarks: Alpha graphs are a notation invented by the American philosopher and logician Charles Sanders Peirce. In this notation, a conjunction of two propositions is written down by simply writing down both propositions. Encircling a proposition negates it. Other connectives need to be expressed by conjunction and negation. E.g. the conditional P->Q is reduced to ~(P&~Q) which looks like this: . This is read as "P scrolls Q".
  There is more information on Peirce's notation in the Stanfort Encyclopaedia of Philosopy.
• Graphical Begriffsschrift notation - The server shows the proposition in the notation introduced by Gottlob Frege in his 1879 Begriffsschrift.
  A few remarks: Frege writes down the conditional P->Q like this: . His negation looks like that: . A text by Stanley N. Burris contains a complete description of Frege's notation.
• Textual expression tree - The server shows the syntactical structure of the proposition entered.
• Textual alpha tree - The server shows an Alpha Graph representing the proposition entered
• Atomic negations - the server generates an equivalent proposition in which only variables are negated.
• Disjunctive normal form (DNF) - the server displays a disjunctive normal form of the proposition entered. A DNF of a proposition is a disjunction of conjunctions of affirmed or denied variables that is equivalent to the proposition.
• Canonical DNF (CDNF) - the canonical DNF of a proposition is the DNF of this proposition each of whose conjunctions exactly once contains every variable occuring in the originating proposition.
• Conjunctive normal form (CNF) - the server displays a conjunctive normal form of the proposition entered. A CNF of a proposition is a conjunction of disjunctions of affirmed or denied variables that is equivalent to the proposition.
• Canonical CNF (CCNF) - the canonical CNF of a proposition is the CNF of this proposition each of whose disjunctions exactly once contains every variable occuring in the originating proposition.
• Prove the proposition - If the proposition entered is a theorem, the server derives it in a natural deduction calculus. If it isn't, it doesn't.
• Eliminate conditionals - the server generates an equivalent proposition that doesn't consist of any conditionals.
• Optimize expression - the proposition is optimized syntactically. Please note that for its best results this optimizer requires the proposition to be a DNF.
• Polish Notation - The proposition is converted to Polish notation.