Skip to main content Skip to main navigation menu Skip to site footer
  • Register
  • Login
  • Language
    • English
    • Język Polski
  • Menu
  • Home
  • Current
  • Archives
  • Online First Articles
  • About
    • About the Journal
    • Submissions
    • Editorial Team
    • Advisory Board
    • Peer Review Process
    • Logic and Logical Philosophy Committee
    • Open Access Policy
    • Privacy Statement
    • Contact
  • Register
  • Login
  • Language:
  • English
  • Język Polski

Logic and Logical Philosophy

On the practical value of Herbrand disjunctions
  • Home
  • /
  • On the practical value of Herbrand disjunctions
  1. Home /
  2. Archives /
  3. No. 8 (2000) /
  4. Articles

On the practical value of Herbrand disjunctions

Authors

  • Uwe Petermann Leipzig University of Applied Sciences

DOI:

https://doi.org/10.12775/LLP.2000.009

Abstract

Herbrand disjunctions are a means for reducing the problem of whether a first-oder formula is valid in an open theory T or not to the problem whether an open formula, one of the so called Herbrand disjunctions, is T -valid or not. Nevertheless, the set of Herbrand disjunctions, which has to be examined, is undecidable in general. Fore this reason the practical value of Herbrand disjunctions has been estimated negatively (cf. [30]). Relying on completeness proofs which are based on the algebraization technique presented in [30], but taking a more optimistic view, we show how Herbrand disjunctions become the base of a method for building in theories into automatic theorem provers [26]. Surveying newer results we discuss how to treat heterogeneous theories [29] as well as practical implications of different normal form transformations.

Author Biography

Uwe Petermann, Leipzig University of Applied Sciences

Dept. of Computer Sciences

References

P. Andrews. Theorem Proving via General Matings. J.ACM 28(2):193–214, 1981.

I. Auffray and P. Enjalbert. Modal theorem proving using equational methods. In Proceedings of Int. Joint Conference on Artificial Intelligence, 1989.

P. Baumgartner. Theory Model Elimination. In H.J. Ohlbach, editor, Proc. GWAI 92, 1992. MP-I-Inf.

P. Baumgartner and U. Petermann. Theory Reasoning. In W. Bibel and P.H. Schmitt, editors, Automated Deduction. A Basis for Applications, volume I, chapter 6, pages 191–224. Kluwer Academic Publishers, 1998.

W. Bibel. Matings in matrices. In J. Siekmann, editor, German Workshop on Artificial Intelligence, pages 171–187, Berlin, 1981. Springer.

W. Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, 1982.

W. Bibel. Computationally improved versions of herbrand’s theorem. In J. Stern, editor, Proceedings of the Herbrand Symposium, pages 11–28, Amsterdam, 1982. North–Holland.

Boyreau. Un atelier de demonstration automatique multilogique. Application a la logique modale et l’unification associativee. PhD thesis, Universit´ e de Caen, 1994.

H.-J. Bürckert. A resolution principle for constrained logics. Artificial Intelligence 66:235–271, 1994.

F. Clerin-Debart. Th´ eories ´ equationelles et de contraintes pour la d´ emonstration automatique en logique multi-modale. PhD thesis, Laboratoire d’Informatique, Universit´ e de Caen, France, Jan. 1992.

daCosta and Dubikajtis. On Ja´ skowski’sDiscussive Logic. In Arruda, da Costa, and Chuaqui, editors, Non-Classical Logics, Model Theory and Computability, pages 37–56. North-Holland, 1977.

F. Debart and P. Enjalbert. A case of termination for associative unification. In J.P.H. Abdulrab, editor, Words Equtions and related Topics: Second International Workshop IWWERT ’91, Berlin, 1992. Springer-Verlag.

F. Debart, P. Enjalbert, and M. Lescot. Multi Modal Logic ProgrammingUsing Equational and Order-Sorted Logic. In M. Okada and S. Kaplan, editors, Proc. 2nd Conf. on Conditional and Typed Rewriting Systems. Springer, 1990. LNCS.

U. Egly. On the value of antiprenexing. Lecture Notes in Computer Science 822:69, 1994.

U. Egly and T. Rath. On the practical value of different normal form transformations. In Proc 12-th CADE. Springer, 1996.

A.M. Frisch and R.B. Scherl. A General Framework for Modal Deduction. In Principles of Knowledge Representation and Reasoning, Proceedings of KR’91, 1991.

W.D. Goldfarb, editor. J. J. Herbrand – Logical writings. Reidel, Dordrecht, 1971.

J.J. Herbrand. Recherches sur la th´ eorie de la d´ emonstration. Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 (Mathem., Phys.), page 128 pp., 1930. Engl. transl. in [17].

S. Jaśkowski. Propositional calculus for contrary deductive systems. Studia Logica 24:143–157, 1969.

S. Kripke. Semantical analysis of modal logic I, normal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 9:67–96, 1963.

D. Loveland. Automated Theorem Proving – A Logical Basis. North Holland, 1978.

D.A. Miller. Proofs in Higher-Order Logic. PhD thesis, Carnegie Mellon University, Pittsburg Pa., 1983.

G. Neugebauer and U. Petermann. Specifications of inference rules and their automatic translation. In Proceedings Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, pages 185–200. Springer, 1995.

G. Neugebauer and T. Schaub. A pool-based connection calculus. In C. Bozsahin, U. Halıcı, K. Oflazar, and N. Yalabık, editors, Proceedings of Third Turkish Symposium on Artificial Intelligence and Neural Networks, pages 297–306. Middle East Technical University Press, 1994.

H.J. Ohlbach and R. Schmidt. Functional translation and second-order frame properties of modal logic. Research Report MPI-I-95-2-002, Max-Planck-Institut für Informatik, Im Stadtwald D 66123 Saarbrücken, jan 1995.

U. Petermann. How to Build-in an Open Theory into Connection Calculi. Journal on Computer and Artificial Intelligence 11(2):105–142, 1992.

U. Petermann. Completeness of the pool calculus with an open built in theory. In G. Gottlob, A. Leitsch, and D. Mundici, editors, 3rd Kurt Gödel Colloquium ’93, volume 713 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

U. Petermann. Building-in hybrid theories. In Proceedings Workshop on First-Order Theorem Proving. RISC Linz, 1997.

U. Petermann. Automated reasoning under hybrid theories. Logic and Logical Philosophy 6:77–107, 1998 (J. Perzanowski, A. Pietruszczak, R. Leszko, and H. Wansing, editors, “The Second German-Polish Workshop on Logic and Logical Philosophy”).

H. Rasiowa and R. Sikorski. The Mathematics of Metamathematics, volume 41 of Monografie Matematyczne. Polish Scientific Publishers, Warsaw, 1970.

Z. Rigó. Untersuchungen zum automatischen Beweisen in Modallogiken. Master’s thesis, Universität Leipzig, 1995.

M. Stickel. Automated deduction by theory resolution. J. of Automated Reasoning 4(1):333–356, 1985.

Downloads

  • PDF

Published

2004-01-18

How to Cite

1.
PETERMANN, Uwe. On the practical value of Herbrand disjunctions. Logic and Logical Philosophy. Online. 18 January 2004. Vol. 8, no. 8, pp. 153-180. [Accessed 6 July 2025]. DOI 10.12775/LLP.2000.009.
  • ISO 690
  • ACM
  • ACS
  • APA
  • ABNT
  • Chicago
  • Harvard
  • IEEE
  • MLA
  • Turabian
  • Vancouver
Download Citation
  • Endnote/Zotero/Mendeley (RIS)
  • BibTeX

Issue

No. 8 (2000)

Section

Articles

Stats

Number of views and downloads: 466
Number of citations: 0

Crossref
Scopus
Google Scholar
Europe PMC

Search

Search

Browse

  • Browse Author Index
  • Issue archive

User

User

Current Issue

  • Atom logo
  • RSS2 logo
  • RSS1 logo

Information

  • For Readers
  • For Authors
  • For Librarians

Newsletter

Subscribe Unsubscribe

Language

  • English
  • Język Polski
Up

Akademicka Platforma Czasopism

Najlepsze czasopisma naukowe i akademickie w jednym miejscu

apcz.umk.pl

Partners

  • Akademia Ignatianum w Krakowie
  • Akademickie Towarzystwo Andragogiczne
  • Fundacja Copernicus na rzecz Rozwoju Badań Naukowych
  • Instytut Historii im. Tadeusza Manteuffla Polskiej Akademii Nauk
  • Instytut Kultur Śródziemnomorskich i Orientalnych PAN
  • Instytut Tomistyczny
  • Karmelitański Instytut Duchowości w Krakowie
  • Ministerstwo Kultury i Dziedzictwa Narodowego
  • Państwowa Akademia Nauk Stosowanych w Krośnie
  • Państwowa Akademia Nauk Stosowanych we Włocławku
  • Państwowa Wyższa Szkoła Zawodowa im. Stanisława Pigonia w Krośnie
  • Polska Fundacja Przemysłu Kosmicznego
  • Polskie Towarzystwo Ekonomiczne
  • Polskie Towarzystwo Ludoznawcze
  • Towarzystwo Miłośników Torunia
  • Towarzystwo Naukowe w Toruniu
  • Uniwersytet im. Adama Mickiewicza w Poznaniu
  • Uniwersytet Komisji Edukacji Narodowej w Krakowie
  • Uniwersytet Mikołaja Kopernika
  • Uniwersytet w Białymstoku
  • Uniwersytet Warszawski
  • Wojewódzka Biblioteka Publiczna - Książnica Kopernikańska
  • Wyższe Seminarium Duchowne w Pelplinie / Wydawnictwo Diecezjalne „Bernardinum" w Pelplinie

© 2021- Nicolaus Copernicus University Accessibility statement Shop