Przejdź do sekcji głównej Przejdź do głównego menu Przejdź do stopki
  • Zarejestruj
  • Zaloguj
  • Język
    • English
    • Język Polski
  • Menu
  • Strona domowa
  • Aktualny numer
  • Archiwum
  • Prace online
  • O czasopiśmie
    • O czasopiśmie
    • Przesyłanie tekstów
    • Zespół redakcyjny
    • Rada redakcyjna
    • Proces recenzji
    • Komitet Logic and Logical Philosophy
    • Polityka Open Access
    • Polityka prywatności
    • Kontakt
  • Zarejestruj
  • Zaloguj
  • Język:
  • English
  • Język Polski

Logic and Logical Philosophy

Theorem proving with built-in hybrid theories
  • Strona domowa
  • /
  • Theorem proving with built-in hybrid theories
  1. Strona domowa /
  2. Archiwum /
  3. Nr 6 (1998) /
  4. Artykuły

Theorem proving with built-in hybrid theories

Autor

  • Uwe Petermann Department of Logic, Nicolaus Copernicus University

DOI:

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

Abstrakt

A growing number of applications of automated reasoning exhibits the necessity of flexible deduction systems. A deduction system should be able to execute inference rules which are appropriate to the given problem. One way to achieve this behavior is the integration of different calculi. This led to so called hybrid reasoning [22, 1, 10, 20] which means the integration of a general purpose foreground reasoner with a specialized background reasoner. A typical task of a background reasoner is to perform special purpose inference rules according to a built-in theory. The aim of this paper is to go a step further, i.e. to treat the background reasoner as a hybrid system itself. The paper formulates sufficient criteria for the construction of complete calculi which enable reasoning under hybrid theories combined from sub-theories. For this purpose we use a generic approach described in [20]. This more detailed view on built-in theories is not covered by the known general approaches [1, 3, 6, 20] for building in theories into theorem provers. The approach is demonstrated by its application to the target calculi of the algebraic translation [9] of multi-modal and extended multi-modal [7] logic to first-order logic.

Biogram autora

Uwe Petermann - Department of Logic, Nicolaus Copernicus University

Dept. of Computer Sciences

Bibliografia

Baumgartner, P., “Theory Model Elimination”, in H. J. Ohlbach (ed.), Proc. GWAI 92, 1992, MP-I-Inf.

Baumgartner, P., Theory Reasoning in Connection Calculi and the Linearizing Completion Approach, PhD thesis, Universität Koblenz-Landau, 1996.

Baumgartner, P., and F. Stolzenburg, “Constraint model elimination and a pttp-implementation”, in Proceedings Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence, 201–216, Springer, 1995.

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

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

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

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

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

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

Frisch, A. M., ‘The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning”, Artificial Intelligence, 1991.

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

Genesereth, M., and N. Nilsson, Logical Foundations of Artificial Intelligence, Morgan Kauffman, Los Altos, California, 1987.

Kripke, S., “Semantical analysis of modal logic I. Normal propositional calculi”, Zeitschrift f¨ur mathematische Logik und Grundlagen der Mathematik 9:67–96, 1963.

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

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

Neugebauer, G., 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, p. 185–200, Springer, 1995.

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

Ohlbach, H. J., 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.

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

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

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

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

Pobrania

  • PDF (English)

Opublikowane

06.11.1998

Jak cytować

1.
PETERMANN, Uwe. Theorem proving with built-in hybrid theories. Logic and Logical Philosophy [online]. 6 listopad 1998, T. 6, nr 6, s. 77–107. [udostępniono 1.7.2025]. DOI 10.12775/LLP.1998.005.
  • PN-ISO 690 (Polski)
  • ACM
  • ACS
  • APA
  • ABNT
  • Chicago
  • Harvard
  • IEEE
  • MLA
  • Turabian
  • Vancouver
Pobierz cytowania
  • Endnote/Zotero/Mendeley (RIS)
  • BibTeX

Numer

Nr 6 (1998)

Dział

Artykuły

Statystyki

Liczba wyświetleń i pobrań: 446
Liczba cytowań: 0

Crossref
Scopus
Google Scholar
Europe PMC

Wyszukiwanie

Wyszukiwanie

Przeglądaj

  • Indeks autorów
  • Lista archiwalnych numerów

Użytkownik

Użytkownik

Aktualny numer

  • Logo Atom
  • Logo RSS2
  • Logo RSS1

Informacje

  • dla czytelników
  • dla autorów
  • dla bibliotekarzy

Newsletter

Zapisz się Wypisz się

Język / Language

  • English
  • Język Polski
W górę

Akademicka Platforma Czasopism

Najlepsze czasopisma naukowe i akademickie w jednym miejscu

apcz.umk.pl

Partnerzy platformy czasopism

  • 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- Uniwersytet Mikołaja Kopernika w Toruniu Deklaracja dostępności Sklep wydawnictwa