Darwin
Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated in tptp or tme format, non-clausal tptp problems are clausified using the eprover. Equality is not built into the currently implemented version of the calculus, it is instead automatically axiomatized for a given problem. Darwin is a decision procedure for function-free clause sets, and is in general faster and scales better on such problems than propositional approaches. Darwin is the first implementation of the Model Evolution Calculus (see papers below). The Model Evolution Calculus lifts the propositional DPLL procedure to first-order logic. One of the main motivations for this approach was the possibility of migrating to the first-order level some of those very effective search techniques developed by the SAT community for the DPLL procedure. The current version of Darwin implements first-order versions of unit propagation inference rules analogously to a restricted form of unit resolution and subsumption by unit clauses. To retain completeness, it includes a first-order version of the (binary) propositional splitting inference rule.
Keywords for this software
References in zbMATH (referenced in 26 articles )
Showing results 1 to 20 of 26.
Sorted by year (- Voigt, Marco: Decidable (\exists^*\forall^*) first-order fragments of linear rational arithmetic with uninterpreted predicates (2021)
- Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
- Confalonieri, Roberto; Kutz, Oliver: Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention (2020)
- Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
- de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
- Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
- Alagi, Gábor; Weidenbach, Christoph: NRCL -- a model building approach to the Bernays-Schönfinkel fragment (2015)
- Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
- Weidenbach, Christoph: Automated reasoning building blocks (2015)
- Hillenbrand, Thomas; Weidenbach, Christoph: Superposition for bounded domains (2013)
- Korovin, Konstantin: Inst-Gen -- a modular approach to instantiation-based automated reasoning (2013)
- Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
- Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
- Déharbe, David; Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno: Exploiting symmetry in SMT problems (2011)
- 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
- Piskac, Ruzica; de Moura, Leonardo; Bjørner, Nikolaj: Deciding effectively propositional logic using DPLL and substitution sets (2010)