13 found
Order:
Disambiguations
Jörg Siekmann [12]J. Siekmann [5]Jörg H. Siekmann [1]
  1.  12
    Proof planning with multiple strategies.Erica Melis, Andreas Meier & Jörg Siekmann - 2008 - Artificial Intelligence 172 (6-7):656-684.
  2.  9
    An order-sorted logic for knowledge representation systems.C. Beierle, U. Hedtstück, U. Pletat, P. H. Schmitt & J. Siekmann - 1992 - Artificial Intelligence 55 (2-3):149-191.
  3.  13
    Knowledge-based proof planning.Erica Melis & Jörg Siekmann - 1999 - Artificial Intelligence 115 (1):65-105.
  4.  18
    Computer supported mathematics with Ωmega.Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2006 - Journal of Applied Logic 4 (4):533-559.
  5.  14
    Natural Language Dialog with a Tutor System for Mathematical Proofs.Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayova, Manfred Pinkal, Jörg Siekmann & Magdalena Wolska - 2007 - In Ruqian Lu, Jörg Siekmann & Carsten Ullrich (eds.), Cognitive Systems: Joint Chinese-German Workshop, Shanghai, China, March 7-11, 2005, Revised Selected Papers. Springer. pp. 1-14.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  17
    Omega.Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet & Jörg Siekmann - 2006 - In Freek Wiedijk (ed.), The Seventeen Provers of the World. Springer. pp. 127-141.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  7.  27
    Jacques Herbrand: life, logic, and automated deduction.Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2009 - In Dov Gabbay (ed.), The Handbook of the History of Logic. Elsevier. pp. 195-254.
    Direct download  
     
    Export citation  
     
    Bookmark  
  8.  26
    Lectures on Jacques Herbrand as a Logician.Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2009 - Seki Publications (Issn 1437-4447).
    We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand’s False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand’s Modus Ponens Elimination. Besides Herbrand’s Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, we carefully investigate Herbrand’s (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  9.  8
    Algorithms in cognition, informatics and logic: A position manifesto.D. Gabbay & J. Siekmann - 2010 - Logic Journal of the IGPL 18 (6):763-768.
  10. History of computational logic.J. Siekmann - 2004 - In Dov M. Gabbay, John Woods & Akihiro Kanamori (eds.), Handbook of the History of Logic. Elsevier. pp. 1.
     
    Export citation  
     
    Bookmark  
  11.  34
    The undecidability of the DA-Unification problem.J. Siekmann & P. Szabó - 1989 - Journal of Symbolic Logic 54 (2):402 - 414.
    We show that the D A -unification problem is undecidable. That is, given two binary function symbols $\bigoplus$ and $\bigotimes$ , variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following D A -axioms hold: \begin{align*}(x \bigoplus y) \bigotimes z &= (x \bigotimes z) \bigoplus (y \bigotimes z),\\x \bigotimes (y \bigoplus z) &= (x \bigotimes y) \bigoplus (x \bigotimes z),\\x \bigoplus (y \bigoplus z) &= (x \bigoplus y) \bigoplus z.\end{align*} Two terms (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  12.  3
    The Undecidability of the $mathrm{D}_mathrm{A}$-Unification Problem.J. Siekmann & P. Szabó - 1989 - Journal of Symbolic Logic 54 (2):402-414.
    We show that the $\mathrm{D_A}$-unification problem is undecidable. That is, given two binary function symbols $\bigoplus$ and $\bigotimes$, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following $\mathrm{D_A}$-axioms hold: \begin{align*}(x \bigoplus y) \bigotimes z &= (x \bigotimes z) \bigoplus (y \bigotimes z),\\x \bigotimes (y \bigoplus z) &= (x \bigotimes y) \bigoplus (x \bigotimes z),\\x \bigoplus (y \bigoplus z) &= (x \bigoplus y) \bigoplus z.\end{align*} Two terms are $\mathrm{D_A}$-unifiable (i.e. an equation (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  13. Reasoning in simple type theory — Festschrift in honor of Peter B. Andrews on his 70th birthday, Studies in Logic, vol. 17. [REVIEW]Christoph Benzmüller, Chad E. Brown, Jörg Siekmann & Richard Statman - 2010 - Bulletin of Symbolic Logic 16 (3):409-411.