@article{Frank2012, author = {Frank, Mario}, title = {Axiom relevance decision engine : technical report}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-72128}, year = {2012}, abstract = {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.}, language = {en} } @article{BrellSeglGuanteretal.2019, author = {Brell, Maximilian and Segl, Karl and Guanter, Luis and Bookhagen, Bodo}, title = {3D hyperspectral point cloud generation}, series = {ISPRS journal of photogrammetry and remote sensing : official publication of the International Society for Photogrammetry and Remote Sensing}, volume = {149}, journal = {ISPRS journal of photogrammetry and remote sensing : official publication of the International Society for Photogrammetry and Remote Sensing}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0924-2716}, doi = {10.1016/j.isprsjprs.2019.01.022}, pages = {200 -- 214}, year = {2019}, abstract = {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.}, language = {en} }