This repository has been archived by the owner on Oct 2, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
verity.1
284 lines (284 loc) · 10.3 KB
/
verity.1
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
.\" Automatically generated by Pod::Man 2.25 (Pod::Simple 3.20)
.\"
.\" Standard preamble:
.\" ========================================================================
.de Sp \" Vertical space (when we can't use .PP)
.if t .sp .5v
.if n .sp
..
.de Vb \" Begin verbatim text
.ft CW
.nf
.ne \\$1
..
.de Ve \" End verbatim text
.ft R
.fi
..
.\" Set up some character translations and predefined strings. \*(-- will
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
.\" double quote, and \*(R" will give a right double quote. \*(C+ will
.\" give a nicer C++. Capital omega is used to do unbreakable dashes and
.\" therefore won't be available. \*(C` and \*(C' expand to `' in nroff,
.\" nothing in troff, for use with C<>.
.tr \(*W-
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
.ie n \{\
. ds -- \(*W-
. ds PI pi
. if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
. if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\" diablo 12 pitch
. ds L" ""
. ds R" ""
. ds C` ""
. ds C' ""
'br\}
.el\{\
. ds -- \|\(em\|
. ds PI \(*p
. ds L" ``
. ds R" ''
'br\}
.\"
.\" Escape single quotes in literal strings from groff's Unicode transform.
.ie \n(.g .ds Aq \(aq
.el .ds Aq '
.\"
.\" If the F register is turned on, we'll generate index entries on stderr for
.\" titles (.TH), headers (.SH), subsections (.SS), items (.Ip), and index
.\" entries marked with X<> in POD. Of course, you'll have to process the
.\" output yourself in some meaningful fashion.
.ie \nF \{\
. de IX
. tm Index:\\$1\t\\n%\t"\\$2"
..
. nr % 0
. rr F
.\}
.el \{\
. de IX
..
.\}
.\"
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
.\" Fear. Run. Save yourself. No user-serviceable parts.
. \" fudge factors for nroff and troff
.if n \{\
. ds #H 0
. ds #V .8m
. ds #F .3m
. ds #[ \f1
. ds #] \fP
.\}
.if t \{\
. ds #H ((1u-(\\\\n(.fu%2u))*.13m)
. ds #V .6m
. ds #F 0
. ds #[ \&
. ds #] \&
.\}
. \" simple accents for nroff and troff
.if n \{\
. ds ' \&
. ds ` \&
. ds ^ \&
. ds , \&
. ds ~ ~
. ds /
.\}
.if t \{\
. ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
. ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
. ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
. ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
. ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
. ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
.\}
. \" troff and (daisy-wheel) nroff accents
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
.ds ae a\h'-(\w'a'u*4/10)'e
.ds Ae A\h'-(\w'A'u*4/10)'E
. \" corrections for vroff
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
. \" for low resolution devices (crt and lpr)
.if \n(.H>23 .if \n(.V>19 \
\{\
. ds : e
. ds 8 ss
. ds o a
. ds d- d\h'-1'\(ga
. ds D- D\h'-1'\(hy
. ds th \o'bp'
. ds Th \o'LP'
. ds ae ae
. ds Ae AE
.\}
.rm #[ #] #H #V #F C
.\" ========================================================================
.\"
.IX Title "VERITY 1"
.TH VERITY 1 "2014-04-01" "Version 1.4" ""
.\" For nroff, turn off justification. Always turn off hyphenation; it makes
.\" way too many mistakes in technical documents.
.if n .ad l
.nh
.SH "NAME"
verity \- generate truth tables of logical statements
.SH "SYNOPSIS"
.IX Header "SYNOPSIS"
\&\fBverity\fR [\fB\-P\fR | \fB\-p\fR | \fB\-t\fR | \fB\-l\fR] [\fB\-s\fR] [\fB\-o\fR \fIoutfile\fR] [\fB\-e\fR \fIstatements\fR | \fIinfile\fR]
.PP
\&\fBverity\fR [\fB\-h\fR | \fB\-V\fR]
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
\&\fBVerity\fR is a utility for generating truth tables for sets of logical
statements. Output can be as plain text, a TeX table, a LaTeX \fItabular\fR
environment, or a PostScript document. The statements can be read from the
standard input or an \fIinfile\fR or simply passed to \fBverity\fR on the command
line as the argument to an \fB\-e\fR flag. The syntax for the statements is
descriped below under \*(L"\s-1STATEMENT\s0 \s-1SYNTAX\s0\*(R".
.SH "OPTIONS"
.IX Header "OPTIONS"
.IP "\fB\-e\fR \fIstatements\fR" 4
.IX Item "-e statements"
\&\fBVerity\fR treats \fIstatements\fR, along with the arguments of any following \fB\-e\fR
switches, as newline-terminated input. If \fIinfile\fR is also specified on the
command line, it is ignored.
.IP "\fB\-h\fR" 4
.IX Item "-h"
Display a summary of the command-line options and exit.
.IP "\fB\-l\fR" 4
.IX Item "-l"
Output is in the form of LaTeX \f(CW\*(C`tabular\*(C'\fR environments. If the \fB\-s\fR option is
also specified, the tabulars are centered.
.IP "\fB\-o\fR \fIoutfile\fR" 4
.IX Item "-o outfile"
Output is written to file \fIoutfile\fR.
.IP "\fB\-P\fR" 4
.IX Item "-P"
Output the tables as a single PostScript document.
.IP "\fB\-p\fR" 4
.IX Item "-p"
Output is as plain text. This is the default.
.IP "\fB\-s\fR" 4
.IX Item "-s"
(La)TeX output is ``standalone,'' i.e., a complete document rather than a
fragment suitable for importing into another document. This option has no
effect on plain text tables or PostScript documents.
.IP "\fB\-t\fR" 4
.IX Item "-t"
Output is in the form of centered TeX tables.
.IP "\fB\-V\fR" 4
.IX Item "-V"
Display version information & exit
.SH "STATEMENT SYNTAX"
.IX Header "STATEMENT SYNTAX"
Statements consist of individual letters (considered case-sensitively)
representing boolean variables and combined with logical \s-1AND\s0 (\f(CW\*(C`^\*(C'\fR, \f(CW\*(C`&\*(C'\fR, or
\&\f(CW\*(C`&&\*(C'\fR), logical inclusive \s-1OR\s0 (\f(CW\*(C`v\*(C'\fR, \f(CW\*(C`|\*(C'\fR, or \f(CW\*(C`||\*(C'\fR), and/or logical exclusive
\&\s-1OR\s0 (\f(CW\*(C`x\*(C'\fR, \f(CW\*(C`X\*(C'\fR, or \f(CW\*(C`+\*(C'\fR) to form logical expressions. (In order to use a
variable named \f(CW\*(C`x\*(C'\fR, \f(CW\*(C`X\*(C'\fR, or \f(CW\*(C`v\*(C'\fR, the letter must be preceded by a
backslash.) Statements may be grouped within parentheses and negated with \f(CW\*(C`\-\*(C'\fR,
\&\f(CW\*(C`!\*(C'\fR, or \f(CW\*(C`~\*(C'\fR. They may also be combined with \f(CW\*(C`\->\*(C'\fR, which results in a
statement which is false if & only if the left statement is true & the right
statement false, and \f(CW\*(C`<\->\*(C'\fR (or \f(CW\*(C`=\*(C'\fR or \f(CW\*(C`==\*(C'\fR), which creates a statement
which is true if & only if both the left & right statements have the same
boolean value. Parentheses and the negation operator have the highest & second
highest precedence, respectively, followed by the \s-1AND\s0, \s-1OR\s0, and \s-1XOR\s0 operators,
then \f(CW\*(C`\->\*(C'\fR, and finally \f(CW\*(C`<\->\*(C'\fR. All binary operators are
left-associative. Whitespace (other than newlines) is ignored.
.PP
Statements are delimited by semicolons or newlines (though a backslash at the
end of a line causes the newline to be ignored, thus letting a single statement
continue over multiple lines), and all statements listed in the input file are
output in the resulting truth table. There is no need to list the variables
explicitly, as any variables used will be automatically placed at the left end
of the table in the order in which they appear in the file. A variable can
have the truth value of a specific statement assigned to it by prefixing the
statement with the variable followed by a colon.
.PP
Multiple tables can be output by grouping the statements for each table between
braces. The set of variables to output will be reset for each table.
.PP
Comments can also be inserted into the input, beginning with a pound sign
(\f(CW\*(C`#\*(C'\fR) and continuing to the end of the line. The end of a line in a comment
does not constitute a statement delimiter, so a semicolon or extra newline is
required if a new statement is to immediately follow.
.SH "EXAMPLES"
.IX Header "EXAMPLES"
The following line causes \fBverity\fR to output the combined truth table for the
statements ``p \s-1AND\s0 q'' and ``p \s-1OR\s0 q'':
.PP
.Vb 1
\& p ^ q; p v q
.Ve
.PP
As plain text, the output for the above is:
.PP
.Vb 6
\& p|q|p^q|pvq
\& \-|\-|\-\-\-|\-\-\-
\& T|T| T | T
\& T|F| F | T
\& F|T| F | T
\& F|F| F | F
.Ve
.PP
For a somewhat more complex example, consider the following statements. Note
that the statement \f(CW\*(C`p || \-q\*(C'\fR is assigned to the variable \f(CW\*(C`S\*(C'\fR for ease of
reference in the statement after it.
.PP
.Vb 4
\& \-p x q
\& S : p || \-q
\& S \-> q&r
\& pvr <\-> !(~p ^ ~r)
.Ve
.PP
When input to \fBverity\fR, the above statements yield the truth table:
.PP
.Vb 10
\& p|q|r|\-pxq|S : pv\-q|S\->q^r|pvr<\->\-(\-p^\-r)
\& \-|\-|\-|\-\-\-\-|\-\-\-\-\-\-\-\-|\-\-\-\-\-\-|\-\-\-\-\-\-\-\-\-\-\-\-\-\-
\& T|T|T| T | T | T | T
\& T|T|F| T | T | F | T
\& T|F|T| F | T | F | T
\& T|F|F| F | T | F | T
\& F|T|T| F | F | T | T
\& F|T|F| F | F | T | T
\& F|F|T| T | T | F | T
\& F|F|F| T | T | F | T
.Ve
.PP
Note that the operator symbols are all reset to ones that resemble the standard
mathematical notation.
.SH "RESTRICTIONS"
.IX Header "RESTRICTIONS"
Assignment of statements to variables with the colon operator should be done
before the variable is used in any other statements. Otherwise, the behavior
is undefined. Similarly, assigning more than one statement to the same
variable also leads to undefined behavior.
.PP
Currently, the PostScript output takes no special steps to deal with tables
going off the edge of the page; if one table reaches the bottom, any tables
after it won't show up.
.SH "SEE ALSO"
.IX Header "SEE ALSO"
<http://github.com/jwodder/Verity>
.SH "AUTHOR"
.IX Header "AUTHOR"
John T. Wodder \s-1II\s0 <jwodder@sdf.lonestar.org>
.SH "COPYRIGHT"
.IX Header "COPYRIGHT"
Copyright 2007, 2008 by John T. Wodder \s-1II\s0
.PP
\&\fBVerity\fR is distributed under the \s-1GNU\s0 General Public License, v.3.0 or later.
There is \s-1NO\s0 warranty; not even for \s-1MERCHANTABILITY\s0 or \s-1FITNESS\s0 \s-1FOR\s0 A \s-1PARTICULAR\s0
\&\s-1PURPOSE\s0.