- Referenced in 6 articles
- complete theorem prover for first order logic with finite Herbrand domains. ModGen takes first order ... problems which are hard for general resolution theorem provers are found easy for ModGen...
- Referenced in 1 article
- Herbrand constructivization for automated intuitionistic theorem proving. We describe a new method to constructivize proofs ... based on Herbrand disjunctions by giving a practically effective algorithm that converts (some) classical first ... Together with an automated classical first-order theorem prover such a method yields an (incomplete...
- Referenced in 279 articles
- ACL2 is both a programming language in which...
- Referenced in 611 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 2917 articles
- Computer algebra system (CAS). Magma is a large...
- Referenced in 5124 articles
- The result of over 30 years of cutting...
- Referenced in 154 articles
- Maxima is a system for the manipulation of...
- Referenced in 536 articles
- An extensible SAT-solver. MiniSat is a minimalistic...
- Referenced in 119 articles
- SETHEO: A high-performance theorem prover. The paper...
- Referenced in 14 articles
- The joint CSCS-ETH/NEC collaboration in parallel...
- Referenced in 1675 articles
- Sage (SageMath) is free, open-source math software...
- Referenced in 71 articles
- TPS and ETPS are, respectively, the Theorem Proving...
- Referenced in 265 articles
- Programming Perl. Perl is a language for easily...
- Referenced in 5 articles
- TGTP: The Great Theorem Prover. ...
- Referenced in 172 articles
- The specification language developed by CoFI is called...
- Referenced in 314 articles
- Our current automated deduction system Otter is designed...
- Referenced in 851 articles
- Haskell is a standardized, general-purpose purely functional...
- Referenced in 290 articles
- Eiffel is an ISO-standardized, object-oriented programming...
- Referenced in 178 articles
- SPASS is an automated theorem prover for first...