Propositional Analyzer

by Martin Kovár, Štěpán Křehlík, Ganna Piddubna

Abstract and usage:

The Propositional Analyzer is a simple handy tool, which can make the process of proving various systems of assertions more easy. It can decide whether a formula of the proposional calculus is a tautological consequence of a set of formulae, used as the assumptions. It also calculates the disjunctive and conjunctive normal forms of the formula F and then minimalize them by the Quine-McCluskey algorithm. The tool can be also helpful in programming and in analysis or construction of various logical circuits.

Input:

Results:

Tautological consequence:

Is T satisfiable?
Is F a tautology?
Is F a contradiction?
Is F a tautological consequence of T?

Complete disjunctive normal form of F:

Minimalized disjunctive normal form of F:

Complete conjunctive normal form of F:

Minimalized conjunctive normal form of F:

The application Propositional Analyzer is written in Java powered by Wolfram webMathematica 3.0. The application is hosted at the server of the Department of Mathematics, Faculty of Electrical Engineering and Communication, Brno University of Technology. For research and scientific activities the software is available free of charge. In all other cases, please contact RNDr. M. Novák, Department of Mathematics, Faculty of Electrical Engineering and Communication, Brno University of Technology, Technická 8, 616 00 Brno, phone: +420 5 4114 3135. Acknowledgement: FEKT-S-11-2/921 "Vlastnosti řešení funkcionálních diferenciálních a diferenčních rovnic"

Enter or modify the set P of atomic formulae :

Enter or modify the set T of assumptions:

Enter or modify the tested formula F:



	The Propositional Analyzer can uderstand to the following symbols for the logical connectives: Imp (implication); Ekv (equivalence); && or And (conjunction), \|\| or Or (disjunction), ! or Not (negation), Xor (xor), Na (nand), Nr (nor).