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 - Rogass, Christian A1 - Segl, Karl A1 - Bookhagen, Bodo A1 - Guanter, Luis T1 - Improving Sensor Fusion: A Parametric Method for the Geometric Coalignment of Airborne Hyperspectral and Lidar Data JF - IEEE transactions on geoscience and remote sensing N2 - Synergistic applications based on integrated hyperspectral and lidar data are receiving a growing interest from the remote-sensing community. A prerequisite for the optimum sensor fusion of hyperspectral and lidar data is an accurate geometric coalignment. The simple unadjusted integration of lidar elevation and hyperspectral reflectance causes a substantial loss of information and does not exploit the full potential of both sensors. This paper presents a novel approach for the geometric coalignment of hyperspectral and lidar airborne data, based on their respective adopted return intensity information. The complete approach incorporates ray tracing and subpixel procedures in order to overcome grid inherent discretization. It aims at the correction of extrinsic and intrinsic (camera resectioning) parameters of the hyperspectral sensor. In additional to a tie-point-based coregistration, we introduce a ray-tracing-based back projection of the lidar intensities for area-based cost aggregation. The approach consists of three processing steps. First is a coarse automatic tie-point-based boresight alignment. The second step coregisters the hyperspectral data to the lidar intensities. Third is a parametric coalignment refinement with an area-based cost aggregation. This hybrid approach of combining tie-point features and area-based cost aggregation methods for the parametric coregistration of hyperspectral intensity values to their corresponding lidar intensities results in a root-mean-square error of 1/3 pixel. It indicates that a highly integrated and stringent combination of different coalignment methods leads to an improvement of the multisensor coregistration. KW - Airborne laser scanning (ALS) KW - coregistration KW - direct georeferencing KW - imaging spectroscopy KW - multisensor KW - parametric georeferencing KW - preprocessing KW - ray tracing KW - rigorous geocoding KW - sensor alignment KW - sensor fusion Y1 - 2016 U6 - https://doi.org/10.1109/TGRS.2016.2518930 SN - 0196-2892 SN - 1558-0644 VL - 54 SP - 3460 EP - 3474 PB - Inst. of Electr. and Electronics Engineers CY - Piscataway ER - TY - JOUR A1 - Brell, Maximilian A1 - Segl, Karl A1 - Guanter, Luis A1 - Bookhagen, Bodo T1 - Hyperspectral and Lidar Intensity Data Fusion: A Framework for the Rigorous Correction of Illumination, Anisotropic Effects, and Cross Calibration JF - IEEE transactions on geoscience and remote sensing N2 - The fusion of hyperspectral imaging (HSI) sensor and airborne lidar scanner (ALS) data provides promising potential for applications in environmental sciences. Standard fusion approaches use reflectance information from the HSI and distance measurements from the ALS to increase data dimen-sionality and geometric accuracy. However, the potential for data fusion based on the respective intensity information of the complementary active and passive sensor systems is high and not yet fully exploited. Here, an approach for the rigorous illumination correction of HSI data, based on the radiometric cross-calibrated return intensity information of ALS data, is presented. The cross calibration utilizes a ray tracing-based fusion of both sensor measurements by intersecting their particular beam shapes. The developed method is capable of compensating for the drawbacks of passive HSI systems, such as cast and cloud shadowing effects, illumination changes over time, across track illumination, and partly anisotropy effects. During processing, spatial and temporal differences in illumination patterns are detected and corrected over the entire HSI wavelength domain. The improvement in the classification accuracy of urban and vegetation surfaces demonstrates the benefit and potential of the proposed HSI illumination correction. The presented approach is the first step toward the rigorous in-flight fusion of passive and active system characteristics, enabling new capabilities for a variety of applications. KW - Airborne laser scanning (ALS) KW - deshadowing KW - imaging spectroscopy KW - in-flight KW - mosaicking KW - pixel-level fusion KW - preprocessing KW - radiometric alignment KW - ray tracing KW - sensor alignment KW - sensor fusion Y1 - 2017 U6 - https://doi.org/10.1109/TGRS.2017.2654516 SN - 0196-2892 SN - 1558-0644 VL - 55 SP - 2799 EP - 2810 PB - Inst. of Electr. and Electronics Engineers CY - Piscataway ER -