summaryrefslogtreecommitdiff
path: root/doc/cvc4.5.in
diff options
context:
space:
mode:
Diffstat (limited to 'doc/cvc4.5.in')
-rw-r--r--doc/cvc4.5.in21
1 files changed, 21 insertions, 0 deletions
diff --git a/doc/cvc4.5.in b/doc/cvc4.5.in
new file mode 100644
index 000000000..d862eec8a
--- /dev/null
+++ b/doc/cvc4.5.in
@@ -0,0 +1,21 @@
+.\" Process this file with
+.\" groff -man -Tascii cvc4.5
+.\"
+.TH CVC4 5 "@MAN_DATE@" "CVC4 release @VERSION@" "Languages documentation"
+.SH NAME
+cvc4 \- the native input language for CVC4
+.SH DESCRIPTION
+.B cvc4
+is an automated theorem prover for first-order formulas with respect
+to background theories of interest.
+
+.SH HISTORY
+.SH "SEE ALSO"
+.BR cvc4 (1),
+.BR libcvc4 (3),
+.BR libcvc4parser (3),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4. It is maintained at
+.BR http://goedel.cs.nyu.edu/wiki/ .
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback