TRAMP

TRAMP: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. The Tramp system transforms the output of several automated theorem provers for first order logic with equality into natural deduction proofs at the assertion level. Through this interface, other systems such as proof presentation systems or interactive deduction systems can access proofs originally produced by any system interfaced by Tramp only by adapting the assertion level proofs to their own needs.


References in zbMATH (referenced in 20 articles , 1 standard article )

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

  1. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  2. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  3. Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří: Lemmatization for stronger reasoning in large theories (2015)
  4. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with (\mathsfFlyspeck) (2014)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2013)
  6. Hetzl, Stefan; Libal, Tomer; Riener, Martin; Rukhaia, Mikheil: Understanding resolution proofs through Herbrand’s theorem (2013)
  7. Rabe, Florian; Kohlhase, Michael; Sacerdoti Coen, Claudio: A foundational view on integration problems (2011)
  8. Byrnes, John; Buchanan, Michael; Ernst, Michael; Miller, Philip; Roberts, Chris; Keller, Robert: Visualizing proof search for theorem prover development (2009) ioport
  9. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  10. Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Combined reasoning by automated cooperation (2008)
  11. Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
  12. Trac, Steven; Puzis, Yury; Sutcliffe, Geoff: An interactive derivation viewer (2007)
  13. Meng, Jia; Quigley, Claire; Paulson, Lawrence C.: Automation for interactive proof: first prototype (2006)
  14. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
  15. Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
  16. Fiedler, Armin: Natural language proof explanation (2005)
  17. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  18. Meier, Andreas; Sorge, Volker; Colton, Simon: Employing theory formation to guide proof planning (2002)
  19. Siekmann, J.; Benzmüller, C.; Fiedler, A.; Meier, A.; Pollet, M.: Proof development with (\Omega)MEGA: (\sqrt2) is irrational (2002)
  20. Meier, Andreas: System description: Tramp. Transformation of machine-found proofs into natural deduction proofs at the assertion level (2000)