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

Showing results 1 to 20 of 33.
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. Blanchette, Jasmin Christian; Popescu, Andrei; Wand, Daniel; Weidenbach, Christoph: More SPASS with Isabelle. Superposition with hard sorts and configurable simplification (2012)
  6. Besson, Frédéric; Cornilleau, Pierre-Emmanuel; Pichardie, David: Modular SMT proofs for fast reflexive checking inside Coq (2011)
  7. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
  8. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  9. Asperti, Andrea; Tassi, Enrico: Higher order proof reconstruction from paramodulation-based refutations: The unit equality case (2007)
  10. Bonichon, Richard; Delahaye, David; Doligez, Damien: Zenon: An extensible automated theorem prover producing checkable proofs (2007)
  11. Paulson, Lawrence C.; Susanto, Kong Woei: Source-level proof reconstruction for interactive theorem proving (2007)
  12. Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène; Blandford, Ann: Providing a formal linkage between MDG and HOL (2007)
  13. Fontaine, Pascal; Marion, Jean-Yves; Merz, Stephan; Nieto, Leonor Prensa; Tiu, Alwen: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants (2006)
  14. Meng, Jia; Quigley, Claire; Paulson, Lawrence C.: Automation for interactive proof: first prototype (2006)
  15. Weber, Tjark: Integrating a SAT solver with an LCF-style theorem prover (2006)
  16. Abel, Andreas; Coquand, Thierry; Norell, Ulf: Connecting a logical framework to a first-order logic prover (2005)
  17. Miller, Swaha; Plaisted, David A.: The space efficiency of OSHL (2005)
  18. Kim, Choon Kyu: Exploiting parallelism: Highly competitive semantic tree theorem prover (2004)
  19. Letz, Reinhold; Stenz, Gernot: Generalised handling of variables in disconnection tableaux (2004)
  20. Meng, Jia; Paulson, Lawrence C.: Experiments on supporting interactive proof using resolution (2004)

1 2 next