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 35 articles )

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

1 2 next

  1. Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
  2. Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef: Hammering towards QED (2016)
  3. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  4. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  5. Harrison, John: The HOL Light theory of Euclidean space (2013)
  6. Kühlwein, Daniel; Schulz, Stephan; Urban, Josef: E-MaLeS 1.1 (2013)
  7. Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph: More SPASS with Isabelle. Superposition with hard sorts and configurable simplification (2012)
  8. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  9. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  10. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  11. Asperti, Andrea; Tassi, Enrico: Higher order proof reconstruction from paramodulation-based refutations: The unit equality case (2007)
  12. Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
  13. Paulson, Lawrence C.; Susanto, Kong Woei: Source-level proof reconstruction for interactive theorem proving (2007)
  14. Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann: Providing a formal linkage between MDG and HOL (2007)
  15. Fontaine, Pascal; Marion, Jean-Yves; Merz, Stephan; Nieto, Leonor Prensa; Tiu, Alwen: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants (2006)
  16. Meng, Jia; Quigley, Claire; Paulson, Lawrence C.: Automation for interactive proof: first prototype (2006)
  17. Weber, Tjark: Integrating a SAT solver with an LCF-style theorem prover (2006)
  18. Abel, Andreas; Coquand, Thierry; Norell, Ulf: Connecting a logical framework to a first-order logic prover (2005)
  19. Miller, Swaha; Plaisted, David A.: The space efficiency of OSHL (2005)
  20. Kim, Choon Kyu: Exploiting parallelism: Highly competitive semantic tree theorem prover (2004)

1 2 next