TY - JOUR A1 - Frank, Mario T1 - Axiom relevance decision engine : technical report N2 - This document presents an axiom selection technique for classic first order theorem proving based on the relevance of axioms for the proof of a conjecture. It is based on unifiability of predicates and does not need statistical information like symbol frequency. The scope of the technique is the reduction of the set of axioms and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the axiom set, it can be used as a preprocessor for automated theorem proving. This technical report describes the conception, implementation and evaluation of ARDE. The selection method, which is based on a breadth-first graph search by unifiability of predicates, is a weakened form of the connection calculus and uses specialised variants or unifiability to speed up the selection. The implementation of the concept is evaluated with comparison to the results of the world championship of theorem provers of the year 2012 (CASC J6). It is shown that both the theorem prover leanCoP which uses the connection calculus and E which uses equality reasoning, can benefit from the selection approach. Also, the evaluation shows that the concept is applyable for theorem proving problems with thousands of formulae and that the selection is independent from the calculus used by the theorem prover. N2 - Dieser technische Report beschreibt die Konzeption, Implementierung und Evaluation eines Verfahrens zur Auswahl von logischen Formeln bezüglich derer Relevanz für den Beweis einer logischen Formel. Das Verfahren wird ausschließlich für die Prädikatenlogik erster Ordnung angewandt, wenngleich es auch für höherstufige Prädikatenlogiken geeignet ist. Das Verfahren nutzt eine unifikationsbasierte Breitensuche im Graphen wobei jeder Knoten im Graphen ein Prädikat und jede existierende Kante eine Unifizierbarkeitsrelation ist. Ziel des Verfahrens ist die Reduktion einer gegebenen Menge von Formeln auf eine für aktuelle Theorembeweiser handhabbare Größe. Daher ist das Verfahren als Präprozess-Schritt für das automatische Theorembeweisen geeignet. Zur Beschleunigung der Suche wird neben der Standard-Unifikation eine abgeschwächte Unifikation verwendet. Das System wurde während der Weltmeisterschaft der Theorembeweiser im Jahre 2014 (CASC J6) in Manchester zusammen mit dem Theorembeweiser leanCoP eingereicht und konnte leanCoP dabei unterstützen, Probleme zu lösen, die leanCoP alleine nicht handhaben kann. Die Tests mit leanCoP und dem Theorembeweiser E im Nachgang zu der Weltmeisterschaft zeigen, dass das Verfahren unabhängig von dem verwendeten Kalkül ist und bei beiden Theorembeweisern positive Auswirkungen auf die Beweisbarkeit von Problemen mit großen Formelmengen hat. KW - Relevanz KW - Graphensuche KW - Theorembeweisen KW - Preprocessing KW - Unifikation KW - relevance KW - graph-search KW - preprocessing KW - unification KW - theorem Y1 - 2012 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-72128 ER - TY - JOUR A1 - Brell, Maximilian A1 - Segl, Karl A1 - Guanter, Luis A1 - Bookhagen, Bodo T1 - 3D hyperspectral point cloud generation BT - Fusing airborne laser scanning and hyperspectral imaging sensors for improved object-based information extraction JF - ISPRS journal of photogrammetry and remote sensing : official publication of the International Society for Photogrammetry and Remote Sensing N2 - Remote Sensing technologies allow to map biophysical, biochemical, and earth surface parameters of the land surface. Of especial interest for various applications in environmental and urban sciences is the combination of spectral and 3D elevation information. However, those two data streams are provided separately by different instruments, namely airborne laser scanner (ALS) for elevation and a hyperspectral imager (HSI) for high spectral resolution data. The fusion of ALS and HSI data can thus lead to a single data entity consistently featuring rich structural and spectral information. In this study, we present the application of fusing the first pulse return information from ALS data at a sub-decimeter spatial resolution with the lower-spatial resolution hyperspectral information available from the HSI into a hyperspectral point cloud (HSPC). During the processing, a plausible hyperspectral spectrum is assigned to every first-return ALS point. We show that the complementary implementation of spectral and 3D information at the point-cloud scale improves object-based classification and information extraction schemes. This improvements have great potential for numerous land cover mapping and environmental applications. KW - Lidar KW - Multispectral point cloud KW - Laser return intensity KW - Unmixing KW - Sharpening KW - Imaging spectroscopy KW - In-flight KW - Pixel level KW - Sensor fusion KW - Data fusion KW - Preprocessing KW - Point cloud segmentation KW - Semantic labeling Y1 - 2019 U6 - https://doi.org/10.1016/j.isprsjprs.2019.01.022 SN - 0924-2716 SN - 1872-8235 VL - 149 SP - 200 EP - 214 PB - Elsevier CY - Amsterdam ER -