Equational Prover. EQP is an automated theorem proving program for first-order equational logic. Its strengths are good implementations of associative-commutative unification and matching, a variety of strategies for equational reasoning, and fast search. It seems to perform well on many problems about lattice-like structures. EQP is not as stable and polished as our main production theorem prover Otter. But it has obtained several interesting results, and we have decided to make it available (including the source code) to everyone, with no restrictions (and of course no warranty). EQP’s documentation is not good, but if you already know Otter, you might not have great difficulty in learning to use EQP.
Keywords for this software
References in zbMATH (referenced in 12 articles )
Showing results 1 to 12 of 12.
- Grabowski, Adam: Lattice theory for rough sets -- a case study with Mizar (2016)
- Schulz, Stephan: Simple and efficient clause subsumption with feature vector indexing (2013)
- Marcinkowski, Jerzy; Otop, Jan; Stelmaszek, Grzegorz: On a semantic subsumption test (2005)
- Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
- Hillenbrand, Thomas: Citius altius fortius: lessons learned from the theorem prover Waldmeister (2003)
- Bonacina, Maria Paola: Combination of distributed search and multi-search in peers-mcd. d. (system description) (2001)
- Melis, E.; Siekmann, J.: Knowledge-based proof planning (1999)
- Bonacina, Maria Paola; Hsiang, Jieh: On the modelling of search in theorem proving -- towards a theory of strategy analysis (1998)
- Dahn, Bernd I.: Robbins algebras are Boolean: A revision of McCune’s computer-generated solution of Robbins problem (1998)
- McCune, William: Automatic proofs and counterexamples for some ortholattice identities (1998)
- Bonacina, Maria Paola: The clause-diffusion theorem prover Peers-mcd (system description) (1997)
- McCune, William: Well-behaved search and the Robbins problem (1997)