Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
KI - Künstliche Intelligenz
Erschienen in: KI - Künstliche Intelligenz 1/2010

01.04.2010 | Fachbeitrag

Instance Based Methods—A Brief Overview

verfasst von: Peter Baumgartner, Evgenij Thorstensen

Erschienen in: KI - Künstliche Intelligenz | Ausgabe 1/2010

Einloggen

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

search-config
loading …

Abstract

Instance-based methods are a specific class of methods for automated proof search in first-order logic. This article provides an overview of the major methods in the area and discusses their properties and relations to the more established resolution methods. It also discusses some recent trends on refinements and applications. This overview is rather brief and informal, but we provide a comprehensive literature list to follow-up on the details.
Vorheriger Artikel Small is Again Beautiful in Description Logics
Nächster Artikel Practical Aspects of Automated Deduction for Program Verification

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!

Jetzt informieren

KI - Künstliche Intelligenz

The Scientific journal "KI – Künstliche Intelligenz" is the official journal of the division for artificial intelligence within the "Gesellschaft für Informatik e.V." (GI) – the German Informatics Society - with constributions from troughout the field of artificial intelligence.

Jetzt informieren

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!

Jetzt informieren
Weitere Produktempfehlungen anzeigen
Fußnoten
1
It took another 25 years until the development of the “modern” theory of resolution had begun in the 1990s [11]. This lead to a breakthrough in resolution theory by unifying more or less all resolution variants and improvements until then in a single theoretical framework, yet more elegant, general and powerful [12].
 
Literatur
1.
Alexander GD (1997) CLIN-E—smallest instance first hyper-linking. J Autom Reason 18(2):177–182 CrossRef
2.
Baumgartner P (1998) Hyper tableaux—the next generation. In: Proc TABLEAUX’98. LNCS, vol 1397, pp 60–76
3.
Baumgartner P (2000) FDPLL—a first order Davis-Putnam-Logeman-Loveland procedure. In: Proc CADE-17. LNAI, vol 1831, pp 200–219
4.
Baumgartner P, Eisinger N, Furbach U (1999) A confluent connection calculus. In: Proc CADE-16. LNAI, vol 1632, pp 329–343
5.
Baumgartner P, Fuchs A, de Nivelle H, Tinelli C (2009) Computing finite models by reduction to function-free clause logic. J Appl Log 7(1):58–74 MATHCrossRefMathSciNet
6.
Baumgartner P, Furbach U, Niemelä I (1996) Hyper tableaux. In: Proc JELIA’96. LNAI, vol 1126
7.
Baumgartner P, Fuchs A, Tinelli C (2006) Implementing the model evolution calculus. Int J Artif Intell Tools 15(1):21–52 CrossRef
8.
Baumgartner P, Fuchs A, Tinelli C (2006) Lemma learning in the model evolution calculus. In: Proc LPAR. LNAI, vol 4246, pp 572–586
9.
Baumgartner P, Fuchs A, Tinelli C (2008) ME(LIA)—model evolution with linear integer arithmetic constraints. In: Proc LPAR’08. LNAI, vol 5330, pp 258–273
10.
Baumgartner P, Waldmann U (2009) Superposition and model evolution combined. In: Proc CADE-22. LNAI, vol 5663, pp 17–34
11.
Bachmair L, Ganzinger H (1990) On restrictions of ordered paramodulation with simplification. In: Proc CADE-10. LNAI, vol 449, pp 427–441
12.
Bachmair L, Ganzinger H (2001) Resolution theorem proving. In: Robinson A, Voronkov A (eds) Handbook of automated reasoning. North-Holland, Amsterdam
13.
Billon J (1996) The disconnection method. In: Proc TABLEAUX’96. LNAI, vol 1071, pp 110–126
14.
Baumgartner P, Schmidt R (2006) Blocking and other enhancements for bottom-up model generation methods. In: Proc IJCAR. LNAI, vol 4130, pp 125–139
15.
Bry F, Torge S (1998) A deduction method complete for refutation and finite satisfiability. In: Proc JELIA. LNAI, pp 122–136
16.
Baumgartner P, Tinelli C (2003) The model evolution calculus. In: Proc CADE-19. LNAI, vol 2741, pp 350–364
17.
Baumgartner P, Tinelli C (2005) The model evolution calculus with equality. In: Proc CADE-20. LNAI, vol 3632, pp 392–408
18.
Cadoli M, Mancini T (2004) Exploiting functional dependencies in declarative problem specifications. In: Proc JELIA”04. LNCS, vol 3229, pp 628–640
19.
Cadoli M, Mancini T (2005) Using a theorem prover for reasoning on constraint problems. In: AI*IA, pp 38–49
20.
Chu H, Plaisted D (1994) Semantically guided first-order theorem proving using hyper-linking. In: Bundy A (ed) Proc CADE-12. LNAI, vol 814, pp. 192–206
21.
Chu H, Plaisted DA (1997) CLIN-S—a semantically guided first-order theorem prover. J Autom Reason 18(2):183–188 CrossRef
22.
Claessen K, Sörensson N (2003) New techniques that improve mace-style finite model building. In: CADE-19 workshop: model computation—principles, algorithms, applications
23.
Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. Commun ACM 5(7)
24.
de Moura L, Bjørner N (2008) Deciding effectively propositional logic using DPLL and substitution sets. In: Proc IJCAR 2008. LNAI, vol 5195, pp 410–425
25.
de Nivelle H, Meng J (2006) Geometric resolution: a proof procedure based on finite model search. In: Proc IJCAR 2006. LNAI, vol 4130
26.
Davis M, Putnam H (1960) A computing procedure for quantification theory. J Assoc Comput Mach 7(3):201–215 MATHMathSciNet
27.
Fermüller C, Pichler R (2001) Model representation via contexts and implicit generalizations. In: Proc LPAR’01. LNCS, vol 2250, pp 409–423
28.
Ganzinger H, Korovin K (2003) New directions in instance-based theorem proving. In: Proc LICS
29.
Ganzinger H, Korovin K (2004) Integrating equational reasoning into instantiation-based theorem proving. In: Proc CSL’04. LNCS, vol 3210, pp 71–84
30.
Ganzinger H, Korovin K (2006) Theory Instantiation. In: Proc LPAR’06. LNCS, vol 4246, pp 497–511
31.
Hooker JN, Rago G, Chandru V, Shrivastava A (2002) Partial instantiation methods for inference in first order logic. J Autom Reason 28(4):371–396 MATHCrossRefMathSciNet
32.
33.
Korovin K (2008) iProver—an instantiation-based theorem prover for first-order logic (system description). In: Proc IJCAR 2008. LNAI, vol. 5195, pp 292–298
34.
Korovin K (2009) Instantiation-based automated reasoning: from theory to practice. In: Proc CADE-22. LNCS, vol 5663, pp 163–166
35.
Lee S (1990) CLIN: an automated reasoning system using clause linking. PhD thesis, The University of North Carolina at Chapel Hill
36.
37.
Letz R, Stenz G (2001) Proof and model generation with disconnection tableaux. In: Proc LPAR’01. LNCS, vol 2250
38.
Letz R, Stenz G (2002) Integration of equality reasoning into the disconnection calculus. In: Proc TABLEAUX 2002. LNCS, vol 2381, pp 176–190
39.
Lynch C, McGregor R (2009) Combining instance generation and resolution. In: Proc FroCoS 2009. LNCS, vol 5749
40.
Manthey R, Bry F (1988) SATCHMO: a theorem prover implemented in prolog. In: Proc CADE-9. LNCS, vol 310, pp 415–434
41.
McCune W (1994) A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problems. Technical report, Argonne National Laboratory
42.
Motik B, Sattler U, Studer R (2004) Query answering for owl-dl with rules. In: International semantic web conference. AAAI Press, Menlo Park, pp 549–563
43.
Mitchell D, Ternovska E, Hach F, Mohebali R (2006) Model expansion as a framework for modeling and solving search problems. Technical report TR 2006-24, Simon Fraser University
44.
Nieuwenhuis R, Rubio A (2001) Paramodulation-based theorem proving. In: Handbook of automated reasoning. Elsevier/MIT Press, Amsterdam/Cambridge, pp 371–443 CrossRef
45.
Navarro Pérez JA, Voronkov A (2007) Encodings of bounded LTL model checking in effectively propositional logic. In: Proc CADE-21. LNCS, vol 4603, pp 346–361
46.
Ranise S, Tinelli C (2006) Satisfiability modulo theories, trends and controversies. IEEE Intell Syst Mag 21(6):71–81 CrossRef
47.
Nonnengart A, Weidenbach C (2001) Computing small clause normal forms. In: Robinson JA, Voronkov A (eds) Handbook of automated reasoning. Elsevier/MIT Press, Amsterdam/Cambridge, pp 335–367
48.
Ohlbach HJ, Schmidt RA (1997) Functional translation and second-order frame properties of modal logics. J Log Comput 7(5):581–603 MATHCrossRefMathSciNet
49.
Peltier N (2003) A more efficient tableaux procedure for simultaneous search for refutations and finite models. In: Proc TABLEAUX 2003. LNCS, vol 2796, pp 181–195
50.
Plaisted D (1994) The search efficiency of theorem proving strategies. In: Bundy A (ed) Proc CADE-12. LNAI, vol 814
51.
52.
Robinson JA (1965) A machine-oriented logic based on the resolution principle. J Assoc Comput Mach 12(1):23–41 MATHMathSciNet
53.
Schmidt RA (1999) Decidability by resolution for propositional modal logics. J Autom Reason 22(4):379–396 MATHCrossRef
54.
Stenz G, Letz R (2004) Generalized handling of variables in disconnection tableaux. In: Proc IJCAR 2004. LNCS, vol 3097, pp 289–306
55.
Slaney J (1994) FINDER: Finite domain enumerator (system description). In: Bundy A (ed) Proc CADE-12. LNAI, vol 814
56.
Stenz G (2002) DCTP 1.2—system abstract. In: Proc TABLEAUX’02. LNAI, vol 2381, pp 335–340
57.
58.
59.
Zhang J, Zhang H (1995) Sem: a system for enumerating models. In: Proc IJCAI-95. Kaufmann, Los Altos, pp 298–303
Metadaten
Titel
Instance Based Methods—A Brief Overview
verfasst von
Peter Baumgartner
Evgenij Thorstensen
Publikationsdatum
01.04.2010
Verlag
Springer-Verlag
Erschienen in
KI - Künstliche Intelligenz / Ausgabe 1/2010
Print ISSN: 0933-1875
Elektronische ISSN: 1610-1987
DOI
https://doi.org/10.1007/s13218-010-0002-x

Weitere Artikel der Ausgabe 1/2010

KI - Künstliche Intelligenz 1/2010 Zur Ausgabe

Projekt

Deductive Verification of System Software in the Verisoft XT Project

Fachbeitrag

Small is Again Beautiful in Description Logics

Dissertationen und Habilitationen

Static Termination Analysis for Prolog Using Term Rewriting and SAT Solving

Community

News

Projekt

Logic-Based Question Answering

Editorial

Künstliche Intelligenz ab 2010 bei Springer

Premium Partner

    Bildnachweise