Last updated August 26, 2000. See the PawEng web page for information on the latest version, or send e-mail to info@paweng.com. Comments or bug-reports are welcome.
PawLogic is a program for manipulating boolean expressions. The program handles both expressions in propositional logic and quantified boolean formulae (QBF).
Logic is widely used today. It forms the basis of mathematical proof methods. It is used in formal verification like symbolic model checking and equivalence checking of combinational and sequential circuits. Logic is also behind product configurators and the construction of remote controls and traffic light intersections. And logic is something we all use daily. For example, most of us readily accept the following reasoning: "If it rains, I get wet. It rains. Therefore I get wet." This is applied logic.
PawLogic lets you work and experiment with logic. If you are a student of logic, you get a valuable tool to aid you in your studies. If you are a professional working with logic, you get an always accessible logic program for you to use whether at the office, at home or on the move. And if you are just interested in the world of logic, here is your chance to get hands-on experience.
PawLogic works under Palm OS 2.0 and higher. Copyright © 2000 Poul F. Williams. All Rights Reserved.
PawLogic is distributed as shareware under one of three different licenses:
The LICENSE file gives the details -- be sure to read it before you install or use PawLogic.
[Top]Before you install PawLogic, make sure that:
PawLogic is distributed as a standard PRC file. Install "PawLogic.prc" like a regular application program using your favorite install tool, for example HotSync for Windows.
[Top]
PawLogic is shareware distributed under one of three different licenses. If you chose License A, then you do not need to register. If you chose License B or License C, then you need to register your use of PawLogic.
The advantages of registration are:
When you register you will receive a registration code. Start PawLogic and select the menu "Help" and the item "Registration". Enter the code at the prompt and press the "Okay" button. That's it!
Please make sure you have the newest version of PawLogic. The newest version will be available on the PawEng web page.
Type of registration Fee in USD Product ID --------------------------------------------------------------- License A (3 variables) none N/A License B (26 variables) $20 134974 License C (2600 variables) $50 134975
Be sure to check the current fees on the PawEng web page.
You can pay by credit card (Visa, Eurocard/Mastercard, American Express, Diners Club), wire transfer, EuroCheque, or cash.
You can pay in either USD or EURO.
The fee is non-refundable.
The registration process is handled by ShareIt! You can register on their secure Internet site, via phone, fax or postal mail.
Go directly to PawLogic's Registration Page. Alternatively you can visit http://www.shareit.com and enter the Product ID.
Select the type of registration you want. Enter your credit card number and the registration code will be sent to you via email.
Call +49-221-2407279. US and Canadian customers may also order by calling toll-free 1-800-903-4152.
Please print out the following form, and fax or mail it to:
element 5 AG / ShareIt!
Vogelsanger Strasse 78
<-- blank line
50823 Koeln
Germany
Phone: +49-221-2407279
Fax: +49-221-2407278
E-mail: register@shareit.com
US checks and cash orders can be sent to the US office:
ShareIt! Inc. PO Box 844 Greensburg, PA 15601-0844 USA Phone: 1-724-850-8186 Fax: 1-724-850-8187
Registration Form for PawLogic ------------------------------ Product ID: 134974 134975 (circle one) Product Name: PawLogic -- License B C (circle one) Last name: __________________________________ First name: __________________________________ Company: __________________________________ Street and #: __________________________________ City, State: __________________________________ Postal code: __________________________________ Country: __________________________________ Phone: __________________________________ Fax: __________________________________ E-Mail: __________________________________ *** Please do not forget to include your e-mail address. **** *** We will use e-mail to communication with you. **** How would you like to receive the registration code? (circle one) e-mail -- fax -- postal mail How would you like to pay the registration fee? (circle one) credit card -- wire transfer -- EuroCheque -- cash Credit card information (if applicable) Credit card: (circle one) Visa -- Eurocard/Mastercard -- American Express -- Diners Club Card holder: __________________________________ Card No.: __________________________________ Expiration Date: ______________________________ Date / Signature: ______________________________[Top]
The main window in PawLogic consists of three lines for entering boolean expressions, a number of popup lists, and a large field for displaying results.
PawLogic accepts boolean expressions in the standard mathematical notation -- slightly adapted due to the character-based interface. Press the DO button to evaluate a formula.
Variables start with 'a', 'b', ..., 'z' and are followed by two digit. For example, "a00", "b42", and "z99" are variables. For convenience, "00" may be skipped, and "00" through "09" may be written as only one digit.
Depending on which license you use, you will have different variables available:
Formulae are written using the following connectives written in order of increasing precedence:
The first line contains biimplication, right implication, left implication, and exclusive or. The remaining lines contain connectives for disjunction, conjunction, and negation. Alternative symbols are listed in parentheses.
Use parentheses to override the precedence of the connectives.
The constants 0 and 1 indicate falsehood and truth.
Use "exist" and "forall" to quantify variables:
exist x : <formula>
forall x : <formula>
exist x,y,z : <formula>
The special variable "ans" always holds the result of the last computation which did not result in an error.
It is possible to store logic functions. PawLogic has 100 slots allocated for such functions. They are called "F00" though "F99". Unnecessary zeros may be dropped.
PawLogic has a generalized version of function application. It is written using square brackets:
Press the "DO" button to evaluate a formula. The result is the smallest set of variables such that, by assigning the variables in the set to 1 and all other variables to 0, the formula evaluates to 1. For a tautology (a formula which is always true), PawLogic displays "true". For a contradiction (a formula which is always false), PawLogic displays "false".
Example: Enter the following expressions and press DO after
each one:
a a or b F1 := exist a : a and b not a a or not aYou should now see the following on your screen:
> a
{a}
> a or b
{a}
> F1 := exist a : a and b
{b}
> not a
{}
> a or not a
true
For example, the "{a}" after "a or b" means that setting variable 'a' to 1 and variable 'b' to 0 makes "a or b" evaluate to 1. The "{}" after "not a" means that setting variable 'a' to 0 makes "not a" evaluate to 1.
The popup list just above the DO button gives you access to the last 25 formulae.
The "oper" popup list gives you access to a number of operators to help you enter formulae quickly.
You can write formulae in the built-in Memo Pad application and load them into PawLogic. Place the formulae in a category named "PawLogic" (without the quotes, but with P and L capitalized). We call a memo with formulae for a "program".
The first word of a program is the name of the collection of formulae. Next follows a series of formulae each terminated with a semicolon. For example:
MyProgram a and not b; F0 := a -> b;
The "prog" popup gives you access to all the programs.
The program name may consist of letters, digits and underscores. However, no spaces are allowed. If you have two or more programs, then their names must differ within the first 32 characters.
Place comments between /* and */:
MyProgram /* Here is a comment */ a and not b; /* Another comment... */ /* ...and yet one */ F0 := a -> b; /* Final comment */
Comments are not allowed before the program name or in the middle of a formula. Place your comments after the program name or after a semicolon.
Select the "Edit" menu and the "Preferences" item to edit your preferences. PawLogic has two options: "Echo programs" and "Singlestep programs".
Choose "Echo programs" to echo each line of a program to the output area.
Choose "Singlestep programs" to execute programs one formula at a time. PawLogic will display each formula and ask whether you want to execute the formula ("step"), execute all remaining formulae without further prompting ("run") or halt the execution of the program ("stop").
[Top]This section contains a number of examples on how to use PawLogic. We urge you to try them out for yourself. Please note that some of them require License B or C as they use other variables than a, b, and c.
For natural numbers, multiplication distributes over addition:
a * (b + c) = a*b + a*cHowever, addition does not distribute over multiplication:
a + b*c != (a+b) * (a+c)The logical operations disjunction and conjunction distribute over one another. To prove it, we write the following program:
distribute F0 := a or (b and c); F1 := (a or b) and (a or c); F2 := a and (b or c); F3 := (a and b) or (a and c); F0 <-> F1; F2 <-> F3;Run the program with the "echo programs" option on. The last two formulae evaluate to "true". Hence, disjunction distributes over conjunction ("F0 <-> F1") and conjunction distributes over disjunction ("F2 <-> F3").
Consider the two formulae:
F0 := (a -> b) and (b -> c) F1 := a -> c
Compute the "exclusive or" between them to find the difference:
F0 <> F1
The result is the set {b}, which means that the variable assignment (a,b,c) = (0,1,0) will show the different between F0 and F1. This can be verified by:
F0[a=0, b=1, c=0] F1[a=0, b=1, c=0]
The first one evaluates to false while the second one evaluates to true.
A stone cannot fly,
Mother cannot fly,
Therefore, Mother is a stone.
(Erasmus Montanus)
The reasoning in the above quote is obviously wrong. But let us prove it!
Let the variable "s" mean "stone", let "f" mean "cannot fly", and let "m" mean "Mother". The sentence "A stone cannot fly" translates to "s -> f". Likewise, "Mother cannot fly" translates to "m -> f". And "Mother is a stone" translates to "m -> s":
F := (s -> f) and (m -> f) -> (m -> s)The formula is not a tautology. Negate it ("not F") to get a counterexample -- one that falsifies F. For example, "m=1", "f=1", "s=0".
We can restate the formula like this: If you from "s" can conclude "f", and you from "m" can conclude "f", then from "m" you can conclude "s". This is not true.
Erasmus Montanus was misusing the law:
(p -> q) and (q -> r) -> (p -> r)
We can restate it like we did above: If you from "p" can conclude "q", and you from "q" can conclude "r", then from "p" you can conclude "r". This is a valid statement -- PawLogic returns "true" if you enter it.
Consider the following two combinational circuits.
The left circuit consists of four NAND gates. The right one consists of two AND, one OR and two NAND gates. Both circuits have four inputs named i1, i2, i3 and i4 and two output. The outputs of the left circuit are named o1' and o2'. The outputs of the right circuit are named o1" and o2".
Are these two circuits equivalent?
By equivalent we mean that they implement the same functions. We do not consider speed, power consumption, glitches, and the like.
We construct a logical model of the circuits. We model the inputs as boolean variables, the gates as boolean connectives, and the outputs as functions. The following program shows our model.
comb F12 := not( i3 and i4 ); F11 := not( not( not( i2 and i3 ) and F12 ) and i1 ); F20 := (i2 and i3) or (i3 and i4); F21 := not( i1 and F20 ); F22 := not( i4 and F20 ); F11 <-> F21; F12 <-> F22;
The functions F11 and F12 correspond to the two outputs of the left circuit. The functions F21 and F22 correspond to the outputs of the right circuit.
The two last lines compare the outputs. Both comparisons give the result "true". This means that the two circuits are indeed equivalent.
Symbolic model checking (SMC) deals with proving temporal properties of systems. The systems are described as state machines and the temporal properties are expressed in a temporal logic. SMC is an active research area throughout the world. We will give a short example of a modulo-4 counter.
The setup is as follows. Periodically we probe an input channel (for example, a keyboard). We distinguish between two cases: Either we get a specific input (say, the user presses the enter key) or we don't. If we get the input we want, we increment a modulo-4 counter. A modulo-4 counter counts 0,1,2,3,0,1,2,3,0,1,2,... Initially the counter is zero. So, our system counts the number of times (modulo 4) the user presses the enter key on the keyboard.
We will use two variables "s0" and "s1" to indicate how far the counter is. (s1,s0) = (0,0) means 0 on the counter. (0,1) means 1, (1,0) means 2, and (1,1) means 3. We let the variable "x" indicate the presence ("x" is true) or absence ("x" is false) of the wanted input.
The following drawing shows the system. The initial state is (0,0). If "x" is true, the system moves to state (0,1). If "x" is also true in the next time slot, then the system moves to (1,0). If, at any point, "x" is not true, the system stays in its current state.
x
(0,0) ------------> (0,1)
^ |
| |
| x | x
| |
| V
x
(1,1) <------------ (1,0)
We will now show that it is possible for the system to reach state (1,1) from the initial state (0,0). This is, of course, easy to see in this simple example. But for larger examples with a hundred or more state variables, it may not be obvious.
First we compute all the states reachable from (0,0). Then we show that (1,1) is among those states.
We will use characteristic functions to represent sets of states. This means that a function "R" represents a set of states --- namely all the states (s1,s0) for which the "R(s1,s0)" is true.
Enter the following program and run it:
init F0 := not s1 and not s0; F2 := x <> s0; F3 := ( ( not x or not s0 ) and s1 ) or ( x and s0 and not s1 ); F1 := ( t0 <-> F2 ) and ( t1 <-> F3 );F0 represents the singleton set {(0,0)}. The function F1 is the characteristic function for the transition relation which relates two states (s1,s0) and (t1,t0) iff there is a transition between them. The function F1 relates the variable t0 to the function F2 and the variable t1 to the function F3.
The function F2 states that if x is false, then t0 is equal to s0. Otherwise t0 has the opposite value of s0. In other words, if x is true, then the low bit alternates. The function F3 says that the high bit stays the same if either x or s0 is false. Otherwise the high bit alternates.
Run the following program:
iter F2 := F0; F0 := exist x, s0, s1 : F0 and F1; F0 := F0[t0=s0, t1=s1] or F2; F0 <-> F2;The first line copies F0 to F2 for later use. The next line computes the states which we can reach in one step from F0. The states are expressed in "t" variables. The following line adjusts to "s" variables and adds the states in F2 (the old states). The final line checks whether we have reached a fixed point. When it evaluates to "true" we are at the fixed point and F0 is the characteristic function for the states reachable from the initial state (0,0).
After the first run of the "iter" program, F0 contains the states (0,0) and (0,1). A second run of "iter" adds the state (1,0). A third run adds (1,1). A fourth run does not add any new states. We are at the fixed point and "F0 <-> F2" evaluate to "true".
Use
(s1 and s0) -> F0to determine that state (1,1) is indeed reachable. [Top]
This section contains information that has absolutely nothing to do with Palm Pilots or handheld computers. But if you are interested in logic, its applications and what goes on behind the scene in logic manipulation programs (like PawLogic), then read on. Otherwise, you can safely skip this section.
The book Model Checking by Edmund Clarke, Orna Grumberg and Doron Peled (330 pages; January 7, 2000; MIT Press; ISBN: 0262032708) gives a good and thorough description of model checking. The authors are leading experts in the field. The book is available at Amazon.com.
Edmund Clarke and his model checking group at Carnegie Mellon University have a webpage with tools and papers.
The Binary Decision Diagram (BDD) data structure and variations of it are commonly used to manipulate boolean expressions. The paper that got it all started was by Randy Bryant. It is called Graph-based algorithms for boolean function manipulation and was published in IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 677-691.
Henrik Reif Andersen has written An Introduction to Binary Decision Diagrams. It is a good starting point if you want to study BDDs.
Jørn Lind-Nielsen has written an efficient BDD-package in C with both a Mosml and a C++ interface. The package is called BuDDy.
Poul Williams (who just happen to be the author of PawLogic) has together with Henrik Reif Andersen and Henrik Hulgaard written a package for manipulating Boolean Expression Diagrams (BEDs). BEDs are closely related to BDDs. The BED package comes with a small shell-like interface for working with BEDs and transforming them to BDDs. This tool has been used at different universities in Advanced Algorithms classes for studying BDDs.
[Top]Avoid doing a soft reset while PawLogic is running. PawLogic's databases may be corrupted. You will need to remove PawLogic and reinstall it.
[Top]Version 1.0.2, August 26, 2000: Fixed some bugs to make it run on OS 3.5. "=>" now works correctly. Introduced "true" and "false" as synonyms for 1 and 0. Programs may now contain comments, and the program name may include digits and underscores. Added a section on related literature to the manual.
Version 1.0.1, August 1, 2000: Formula display changed from 10 to 9 lines to avoid a one pixel overlap between the lines. The web site and email has been changed from PawSoft to PawEng.
Version 1.0, June 27, 2000: First release.
[Top]