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: ...

References in zbMATH (referenced in 23 articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  2. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  3. Harrison, John: The HOL Light theory of Euclidean space (2013)
  4. Kühlwein, Daniel; Schulz, Stephan; Urban, Josef: E-MaLeS 1.1 (2013)
  5. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  6. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  7. Asperti, Andrea; Tassi, Enrico: Higher order proof reconstruction from paramodulation-based refutations: The unit equality case (2007)
  8. Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
  9. Paulson, Lawrence C.; Susanto, Kong Woei: Source-level proof reconstruction for interactive theorem proving (2007)
  10. Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann: Providing a formal linkage between MDG and HOL (2007)
  11. Fontaine, Pascal; Marion, Jean-Yves; Merz, Stephan; Nieto, Leonor Prensa; Tiu, Alwen: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants (2006)
  12. Meng, Jia; Quigley, Claire; Paulson, Lawrence C.: Automation for interactive proof: first prototype (2006)
  13. Weber, Tjark: Integrating a SAT solver with an LCF-style theorem prover (2006)
  14. Abel, Andreas; Coquand, Thierry; Norell, Ulf: Connecting a logical framework to a first-order logic prover (2005)
  15. Letz, Reinhold; Stenz, Gernot: Generalised handling of variables in disconnection tableaux (2004)
  16. Meng, Jia; Paulson, Lawrence C.: Experiments on supporting interactive proof using resolution (2004)
  17. Mhamdi, Tarek; Tahar, Sofiène: Providing automated verification in HOL using MDGs (2004)
  18. Deplagne, Eric; Kirchner, Claude; Kirchner, Hélène; Nguyen, Quang Huy: Proof search and proof check for equational and inductive theorems. (2003)
  19. Norrish, Michael: Complete integer decision procedures as derived rules in HOL (2003)
  20. Melham, T.F.: PROSPER. An investigation into software architecture for embedded proof engines (2002)

1 2 next