Complete Guide: Installing prover9 on Ubuntu 16.04 LTS (Xenial Xerus) 2024

1. Install "prover9" package

This guide let you learn how to install prover9 on Ubuntu 16.04 LTS (Xenial Xerus)


    
        
            $
        

        
            
                sudo apt update
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt install
            
                        
                prover9
            
                    
    
    Copied

2. Uninstall "prover9" package

This is a short guide on how to uninstall prover9 on Ubuntu 16.04 LTS (Xenial Xerus):


    
        
            $
        

        
            
                sudo apt remove
            
                        
                prover9
            
                    
    
    Copied


    
        
            $
        

        
            
                sudo apt autoclean && sudo apt autoremove
            
                    
    
    Copied

3. Information about the prover9 package on Ubuntu 16.04 LTS (Xenial Xerus)

Package: prover9
Priority: optional
Section: universe/math
Installed-Size: 299
Maintainer: Ubuntu Developers
Original-Maintainer: Debian QA Group
Architecture: amd64
Source: ladr
Version: 0.0.200911a-2.1
Depends: libc6 (>= 2.11), libladr4 (>= 0.0.200911a-1)
Suggests: ladr4-apps (= 0.0.200911a-2.1), prover9-doc (>> 0.0.200902a), prover9-doc (<< 0.0.200902b)
Filename: pool/universe/l/ladr/prover9_0.0.200911a-2.1_amd64.deb
Size: 75358
MD5sum: 53e509842e49c8a5b4aadd3b01444336
SHA1: 819db8b95e600b4758e9f0d933793277142bbe4c
SHA256: 75e19f3035bfb2f6b7063b0e2ba532b66af48fd10a4dc0a70b0f11551820dee7
Description-en: theorem prover and countermodel generator
This package provides the Prover9 resolution/paramodulation theorem
prover and the Mace4 countermodel generator.
.
Prover9 is an automated theorem prover for first-order and equational
logic. It is a successor of the Otter prover. Prover9 uses the
inference techniques of ordered resolution and paramodulation with
literal selection.
.
The program Mace4 searches for finite structures satisfying first-order
and equational statements, the same kind of statement that Prover9
accepts. If the statement is the denial of some conjecture, any
structures found by Mace4 are counterexamples to the conjecture.
.
Mace4 can be a valuable complement to Prover9, looking for
counterexamples before (or at the same time as) using Prover9 to search
for a proof. It can also be used to help debug input clauses and formulas
for Prover9.
Description-md5: c442e7a696a012e3623fe548e18e8471
Homepage: http://www.cs.unm.edu/~mccune/mace4/
Bugs: https://bugs.launchpad.net/ubuntu/+filebug
Origin: Ubuntu