Gandalf
Gandalf is an automated theorem proving (ATP) system. It proves theorems formulated in logic. Since logic is a pretty universal language, ATP systems such as Gandalf can prove theorems in mathematics and verify complex systems such as digital circuits, software and communications protocols. A new application area for ATP systems is the Semantic Web: a project to bring machine-understandable content to the web. andalf has been in development since 1995. It has participated in the yearly CASC competitions for ATP systems, with impressive results, see CASC: ...
Keywords for this software
References in zbMATH (referenced in 23 articles )
Showing results 1 to 20 of 23.
Sorted by year (- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
- Harrison, John: The HOL Light theory of Euclidean space (2013)
- Kühlwein, Daniel; Schulz, Stephan; Urban, Josef: E-MaLeS 1.1 (2013)
- Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
- Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
- Asperti, Andrea; Tassi, Enrico: Higher order proof reconstruction from paramodulation-based refutations: The unit equality case (2007)
- Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
- Paulson, Lawrence C.; Susanto, Kong Woei: Source-level proof reconstruction for interactive theorem proving (2007)
- Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann: Providing a formal linkage between MDG and HOL (2007)
- Fontaine, Pascal; Marion, Jean-Yves; Merz, Stephan; Nieto, Leonor Prensa; Tiu, Alwen: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants (2006)
- Meng, Jia; Quigley, Claire; Paulson, Lawrence C.: Automation for interactive proof: first prototype (2006)
- Weber, Tjark: Integrating a SAT solver with an LCF-style theorem prover (2006)
- Abel, Andreas; Coquand, Thierry; Norell, Ulf: Connecting a logical framework to a first-order logic prover (2005)
- Letz, Reinhold; Stenz, Gernot: Generalised handling of variables in disconnection tableaux (2004)
- Meng, Jia; Paulson, Lawrence C.: Experiments on supporting interactive proof using resolution (2004)
- Mhamdi, Tarek; Tahar, Sofiène: Providing automated verification in HOL using MDGs (2004)
- Deplagne, Eric; Kirchner, Claude; Kirchner, Hélène; Nguyen, Quang Huy: Proof search and proof check for equational and inductive theorems. (2003)
- Norrish, Michael: Complete integer decision procedures as derived rules in HOL (2003)
- Melham, T.F.: PROSPER. An investigation into software architecture for embedded proof engines (2002)