[PATCH] gnu: aris: New function

[John Darrington <jmd@gnu.org>]

* gnu/packages/maths.scm (aris): New package
---
 gnu/packages/maths.scm |   27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 49fdace..db77fc2 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -589,3 +589,30 @@ library routines perform an LU decomposition with partial pivoting and
 triangular system solves through forward and back substitution.  The library
 also provides threshold-based ILU factorization preconditioners.")
     (license license:bsd-3)))
+
+(define-public aris
+  (package
+    (name "aris")
+    (version "2.2")
+    (source
+     (origin
+      (method url-fetch)
+      (uri (string-append "mirror://gnu/aris/aris-" version ".tar.bz2"))
+      (sha256
+       (base32
+        "0ywfdqnqxabk2293g4ahyh20jr5sw6ac14najdw99z5qm919px7f"))))
+    (build-system gnu-build-system)
+    (inputs
+     `(("gtk+" ,gtk+)
+       ("libxml2" ,libxml2)))
+    (native-inputs
+     `(("pkg-config" ,pkg-config)))
+    (home-page "http://www.gnu.org/software/aris/")
+    (synopsis "Natural deduction first-order logic interface")
+    (description "Aris is a program for performing logical proofs.  It supports
+propositional and predicate logic, as well as Boolean algebra and
+arithmetical logic.  In addition to its predefined inference and equivalence
+rules, Aris also supports references to older proofs. Its use of standard
+logical symbols and its natural deduction interface make it easy to use for
+beginners.")
+    (license license:gpl3+)))
-- 
1.7.10.4