Portal de Periódicos da CAPES

E - a brainiac theorem prover

2002; IOS Press; Volume: 15; Issue: 2 Linguagem: Inglês

1875-8452

Stephan Schulz,

Formal Methods in Verification

We describe the superposition-based theorem prover E. E is a sound and complete prover for clausal first order logic with equality. Important properties of the prover include strong redundancy elimination criteria, the DISCOUNT loop proof procedure, a very flexible interface for specifying search control heuristics, and an efficient inference engine. We also discuss strength and weaknesses of the system.