E-Darwin is an automated theorem prover for first-order clausal logic with equality. It accepts problems in tptp or tme syntax. Non-clausal input is clausified using the eprover (or soon a built-in clausifier). E-Darwin implements the Model Evolution calculus and several variants thereof which include equality reasoning, see the papers. The system is a based on the Darwin prover. As Darwin is no longer actively maintained, E-Darwin will eventually subsume all of its functions. The development of E-Darwin forked off from Darwin 1.3, so at the moment E-Darwin still needs to catch up on the changes made between Darwin 1.3 and its last version, Darwin 1.4.5.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
- Lisitsa, Alexei: Finite reasons for safety (2013)
- Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
- Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter: The TPTP typed first-order form with arithmetic (2012)
- Gebser, Martin; Sabuncu, Orkunt; Schaub, Torsten: An incremental answer set programming based system for finite model computation (2011)
- Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
- Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare: Computing finite models by reduction to function-free clause logic (2009)
- Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare: Lemma learning in the model evolution calculus (2006)