Skip to main content

2016 | OriginalPaper | Buchkapitel

On the Deduction Problem in Gödel and Product Logics

verfasst von : Dušan Guller

Erschienen in: Computational Intelligence

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We investigate the deduction problem in Gödel and Product logics, both equipped with Gödel negation, in the countable case. Our approach is based on translation of a formula to an equivalent satisfiable finite order clausal theory, consisting of order clauses. An order clause is a finite set of order literals of the form \(\varepsilon _1\diamond \varepsilon _2\) where \(\diamond \) is a connective either https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq3_HTML.gif or \(\prec \). https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq5_HTML.gif and \(\prec \) are interpreted by th xe equality and standard strict linear order on [0, 1], respectively. We generalise the well-known hyperresolution principle to the standard first-order Gödel logic and devise a calculus operating over order clausal theories. A variant of the DPLL procedure in the propositional Product logic exploiting trichotomy and operating over order clausal theories, will be proposed. Both the calculi are refutation sound and complete for the countable case.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
2
We assume a decreasing connective and quantifier precedence: \(\forall \), \(\exists \), \(\lnot \), \(\wedge \), \(\rightarrow \), https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq66_HTML.gif , \(\prec \), \(\vee \).
 
3
We assume a decreasing operator precedence: https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq88_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq89_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq90_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq91_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq92_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq93_HTML.gif .
 
6
We assume a decreasing connective precedence: \(\lnot \),&, \(\wedge \), \(\rightarrow \), https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq761_HTML.gif , \(\prec \), \(\vee \).
 
7
We assume a decreasing operator precedence: https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq781_HTML.gif , \({\cdot }\), https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq783_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq784_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq785_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq786_HTML.gif , https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-23392-5_17/978-3-319-23392-5_17_IEq787_HTML.gif .
 
Literatur
1.
Zurück zum Zitat Metcalfe, G., Olivetti, N., Gabbay, D.M.: Analytic calculi for product logics. Arch. Math. Log. 43, 859–890 (2004) MathSciNetCrossRef Metcalfe, G., Olivetti, N., Gabbay, D.M.: Analytic calculi for product logics. Arch. Math. Log. 43, 859–890 (2004) MathSciNetCrossRef
2.
Zurück zum Zitat Savický, P., Cignoli, R., Esteva, F., Godo, L., Noguera, C.: On product logic with truth-constants. J. Log. Comput. 16, 205–225 (2006) MathSciNetCrossRef Savický, P., Cignoli, R., Esteva, F., Godo, L., Noguera, C.: On product logic with truth-constants. J. Log. Comput. 16, 205–225 (2006) MathSciNetCrossRef
3.
Zurück zum Zitat Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293–304 (1986) MathSciNetCrossRef Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293–304 (1986) MathSciNetCrossRef
4.
5.
6.
Zurück zum Zitat Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction—CADE-15, Proceedings of 15th International Conference on Automated Deduction., Lindau, Germany. Lecture Notes in Computer Science, vol. 1421, pp. 397–411. Springer, 5–10 July 1998 Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction—CADE-15, Proceedings of 15th International Conference on Automated Deduction., Lindau, Germany. Lecture Notes in Computer Science, vol. 1421, pp. 397–411. Springer, 5–10 July 1998
7.
Zurück zum Zitat Guller, D.: A DPLL procedure for the propositional Gödel logic. In: Filipe, J., Kacprzyk, J. (eds.) ICFC-ICNC 2010—Proceedings of the International Conference on Fuzzy Computation and International Conference on Neural Computation (Parts of the International Joint Conference on Computational Intelligence IJCCI 2010), Valencia, Spain, pp. 31–422. SciTePress, 4–26 Oct 2010 Guller, D.: A DPLL procedure for the propositional Gödel logic. In: Filipe, J., Kacprzyk, J. (eds.) ICFC-ICNC 2010—Proceedings of the International Conference on Fuzzy Computation and International Conference on Neural Computation (Parts of the International Joint Conference on Computational Intelligence IJCCI 2010), Valencia, Spain, pp. 31–422. SciTePress, 4–26 Oct 2010
Metadaten
Titel
On the Deduction Problem in Gödel and Product Logics
verfasst von
Dušan Guller
Copyright-Jahr
2016
Verlag
Springer International Publishing
DOI
https://doi.org/10.1007/978-3-319-23392-5_17