LuxLogAI 2018: Papers with Abstracts

Papers
On Inductive Verification and Synthesis Dennis Peuter and Viorica Sofronie-Stokkermans Abstract. We study possibilities of using symbol elimination in program verification and synthesis. We consider programs for which a property is given, which is supposed to hold for all states reachable from the initial states. If it can not be proven that such a formula is an inductive invariant, the task is to find conditions to strengthen the property in order to make it an inductive invariant. We propose a method for property-directed invariant generation and analyze its properties.
Competitive Proving for Fun Maximilian Paul Louis Haslbeck and Simon Wimmer Abstract. We propose a system for large-scale theorem proving contests. We hope that such contests could spark interest in the research field, attract a new generation of theorem proving savants, and foster competition among proof assistants. For the proof assistant Isabelle, we construct and evaluate two iterations of a prototype implementation of our proposed system architecture.
A Roadmap to Gradually Compare and Benchmark Description Logic Calculi Fred Freitas Abstract. DL reasoners were developed with cutting-edge performance, implementing plenty of specific optimization techniques over tableaux-based methods, which took over the field. However, promising methods may have been neglected in such a scenario, in which the tough competition is often focused on gains through optimizations. Therefore, perhaps there is still room available for “basic research” on DL reasoning. The purpose of this work is to stimulate research on trying out DL calculi other than tableaux. Such endeavors should be carried out by making a careful, detailed comparison between tableaux and other inference methods in a systematic way: first starting with simpler languages (like ALC) without any optimizations. Then gradually including optimizations and comparing them; and continuing these interactive steps: enhancing language expressivity, including optimizations, and testing until reaching the most expressive DL fragments such as SROIQ. The comparison can also be done by in terms memory usage and algorithm asymptotic analysis, with worst and average cases, etc. The rationale is identifying whether there are fragments which are more suitable to certain inference methods, as well as which aspects or constructs (e.g., the costliest combinations, which usually involve inverses, nominals, equalities, etc) are sensitive to which calculus.
CoRg: Commonsense Reasoning Using a Theorem Prover and Machine Learning Sophie Siebert and Frieder Stolzenburg Abstract. Commonsense reasoning is an everyday task that is intuitive for humans but hard to implement for computers. It requires large knowledge bases to get the required data from, although this data is still incomplete or even inconsistent. While machine learning algorithms perform rather well on these tasks, the reasoning process remains a black box. To close this gap, our system CoRg aims to build an explainable and well-performing system, which consists of both an explainable deductive derivation process and a machine learning part. We conduct our experiments on the Copa question-answering benchmark using the ontologies WordNet, Adimen-SUMO, and ConceptNet. The knowledge is fed into the theorem prover Hyper and in the end the conducted models will be analyzed using machine learning algorithms, to derive the most probable answer.
Leibniz on Reasoning about Impossible Concepts Lukas Grätz Abstract. Leibniz wrote down a proof for the existence of God accompanied by a note on im- possible concepts. A possibly true contradiction is quite unusual and not compatible with mainstream logic or his “Theodicy”. His example of such a contradiction about an impossible concept, the “square circle”, is still popular in contemporary metaphysics. Similar examples make the proposition of contradiction and possible truth controversial. An alter- native formalization approach avoids contradictions by using a description logics extension to a different kind of concept composition.
An Ontology for Transportation System Durgesh Nandini and Gautam Kishore Shahi Abstract. In this work, we present a domain ontology for Transportation System. We have developed an ontology for a semantics-aware transportation system from the perspective of a traveler user, capable of answering general competence queries like the nearest bus stop to a particular place, the nearest parking slots available, etc. We have studied the transportation system of some of the big cities of the world and have tried to come up with a vocabulary that can be applied to any city with little modifications. This vocabulary is further aligned with an upper-level ontology to have a common starting point.
Inducing Schema.org markup from Natural Language Context Gautam Kishore Shahi, Durgesh Nandini and Sushma Kumari Abstract. Schema.org creates, supports and maintain schemas for structured data on the web pages. For a non-technical author, it is difficult to publish contents in a structured format. This work presents an automated way of inducing Schema.org markup from natural language context of web-pages by applying knowledge base creation technique. As a dataset, Web Data Commons was used, and the scope for the experimental part was limited to RDFa. The approach was implemented using the Knowledge Graph building techniques - Knowledge Vault and KnowMore.
Concepts as Modalities in Description Logics Lukas Grätz Abstract. Motivated by the colloquial language term of a “glass gummy bear”, an additional type of concept composition for description logics is suggested. This composition type is then axiomatically formalized and called concept generalization. Consistency of the formalization is checked. By proving axiom K and Go ̈del rule, it is shown that this logic is in fact a multi-modal logic. Concepts could be both modal operators and predicate symbols. A Kripke semantics is presented (the adequacy is future work). In this semantics, the TBox axioms hold for any view, assertions in the ABox hold for the natural view (a selected world in the Kripke structure) only. The relationship to other formalisms is outlined. Further examples are discussed at the end.