This book constitutes the refereed proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 200, held in Munich, Germany, in August 2009. The 26 revised full papers presented together with 1 proof pearl, 4 tool presentations, and 3 invited papers were carefully reviewed and selected from 55 submissions.

The papers cover all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification such as formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalization of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.

This book constitutes the proceedings of the 6th International Conference on Interactive Theorem Proving, ITP 2015, held in Nanjing, China, in August 2015. The 27 papers presented in this volume were carefully reviewed and selected from 54 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.

Bachelorarbeit aus dem Jahr 2003 im Fachbereich Informatik - Software, Note: 1,7, Otto-von-Guericke-Universitat Magdeburg (Informatik), Sprache: Deutsch, Abstract: Inhaltsangabe: Einleitung: Das Ziel dieses Praktikums ist es, unter Berucksichtigung der Phasen der Softwareentwicklung, eine Webanwendung zur effizienten Recherche in der Lost Art Internet Datenbank zu entwerfen und einzelne Module zu implementieren. Die Webanwendung soll den vollstandigen Rechercheprozess, angefangen von der Vorverarbeitung der Daten bis hin zur Reprasentation der Ergebnisse unterstutzen. Auch fur bereits existierende Abbildungen muss die Moglichkeit bestehen diverse Feature (z.B. Farbe oder Textur) zu extrahierten und diese in einer Datenbank abzulegen. Der Nutzer soll die Moglichkeit bekommen die Ahnlichkeitssuche, die Suche nach Objekten und die textbasierte Suche einzeln oder in Kombination einzusetzen. Das heisst das System muss in der Lage sein auch komplexe Nutzeranfragen zu bearbeiten, die aus mehreren Anfragetermen zusammengesetzt sind. Aufgrund dieser Anforderungen ist ein wesentlicher Bestandteil der Arbeit die Vorverarbeitung der Daten und die dazu gehorende Entwicklung von Programmmodulen zur Bildsegmentierung, Verschlagwortung, Featureextraktion und Bestimmung der Lagebeziehungen. Da vollautomatische Objekterkennungssysteme, die z.B. mit dem Split and Merge Algorithmus arbeiten, nicht immer die gewunschten Ergebnisse liefern und das manuelle Nachzeichnen von Objektkanten ungenau und sehr zeitintensiv ist, soll ein semiautomatisches Segmentierungstool entwickelt werden, das den Benutzer bei dieser Aufgabe unterstutzt. Ein weiterer wichtiger Aspekt ist die Entwicklung eines Recherchesystems mit den entsprechenden Schnittstellen zur Integration der Programmkomponenten. Am Ende des Rechercheprozesses sollen dem Nutzer die Abbildungen, die eine Ahnlichkeit von beispielsweise 90 Prozent aufweisen, in entsprechender Reihenfolge prasentiert werden. Um in das Lost Art Projekt integ