|
|
|
|
| LEADER |
02053nmm a2200241 u 4500 |
| 001 |
EB000701491 |
| 003 |
EBX01000000000000000554573 |
| 005 |
00000000000000.0 |
| 007 |
cr||||||||||||||||||||| |
| 008 |
140122 ||| ger |
| 020 |
|
|
|a 9783663076810
|
| 100 |
1 |
|
|a Kutsche, Ralf-Detlef
|
| 245 |
0 |
0 |
|a Grundlagen des maschinellen Beweisens
|h Elektronische Ressource
|b Eine Einführung für Informatiker und Mathematiker
|c von Ralf-Detlef Kutsche
|
| 250 |
|
|
|a 2nd ed. 1991
|
| 260 |
|
|
|a Wiesbaden
|b Vieweg+Teubner Verlag
|c 1991, 1991
|
| 300 |
|
|
|a IX, 174 S. 15 Abb
|b online resource
|
| 505 |
0 |
|
|a l Grundbegriffe der Prädikatenlogik -- 1.1 Syntax der Prädikatenlogik -- 1.2 Semantik der Prädikatenlogik -- 1.3 Normierung der Syntax: Gentzenformeln und die Schnittregel -- 1.4 Normierung der Semantik: Herbrand-Strukturen -- 1.5 Korrektheit und Vollständigkeit -- 1.6 Theorembeweisen durch Widerlegungen -- 2 Resolution -- 2.1 Unifikation -- 2.2 Resolution und Faktorisierung -- 3 Einschränkung des Suchraums -- 3.1 Der Suchraum -- 3.2 Allgemeine Konzepte -- 3.3 Strukturelle Konzepte -- 3.4 Ordnungskonzepte -- 3.5 Semantische Konzepte -- 3.6 Kombination von Konzepten -- 4 Repräsentation des Suchraums -- 4.1 Connection-Graph-Resolution -- 4.2 Matrix-Verfahren -- 4.3 Tableau-Verfahren -- 5 Paramodulation -- 5.1 Gleichheit -- 5.2 Paramodulation -- 6 Termersetzung: Grundlagen -- 6.1 Termersetzungssysteme -- 6.2 Ersetzungssysteme: Termination und Konfluenz -- 6.3 Lokale Konfluenz und kritische Paare -- 7 Termersetzung: Spezielle Techniken -- 7.1 Terminationskriterien -- 7.2 Knuth-Bendix-Vervollständigung -- 7.3 Induktive Beweise -- 7.4 Lösen von Gleichungen: Narrowing -- 7.5 Beweisen in speziellen Gleichheitstheorien -- Schlußbemerkungen -- Literatur -- Symbolverzeichnis -- Sachwortverzeichnis
|
| 653 |
|
|
|a Engineering
|
| 653 |
|
|
|a Engineering, general
|
| 041 |
0 |
7 |
|a ger
|2 ISO 639-2
|
| 989 |
|
|
|b SBA
|a Springer Book Archives -2004
|
| 856 |
4 |
0 |
|u https://doi.org/10.1007/978-3-663-07681-0?nosfx=y
|x Verlag
|3 Volltext
|
| 082 |
0 |
|
|a 620
|