Search

This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs., 11 pages, 7 appendices (data, proofs and links to proofs); to appear in the Logic Journal of the IGPL

The logic embedding tool provides a procedural encoding for non-classical reasoning problems into classical higher-order logic. It is extensible and can support an increasing number of different non-classical logics as reasoning targets. When used as a pre-processor or library for higher-order theorem provers, the tool admits off-the-shelf automation for logics for which otherwise few to none provers are currently available., 10 pages, 1 figure, 1 table

Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastructure for automated theorem proving, the TPTP World, currently supports only classical logics. Similar standards for non-classical logic reasoning do not exist (yet). This hampers practical development of reasoning systems, and limits their interoperability and application. This paper describes the latest extension of the TPTP World, which provides languages and infrastructure for reasoning in non-classical logics. The extensions integrate seamlessly with the existing TPTP World., Comment: 21 pages

Input/Output (I/O) logics address the abstract study of conditional norms. Here, norms are represented as pairs of formulas instead of statements that themselves carry truth-values. I/O logics have been studied thoroughly in the past, including further applications and refinements. In this paper, a class of automated reasoning procedures is presented that, given a set of norms and a concrete situation, decide whether a specific state of affairs is obligatory according to the output operations of I/O logics. The procedures are parametric in the underlying logical formalism and can be instantiated with different classical objects logics, such as propositional logic or first-order logic. The procedures are shown to be correct, and a proof-of-concept implementation for propositional I/O logics is surveyed.

Argumentation frameworks constitute the central concept of argumentation theory of Dung. In this paper we present a novel and flexible approach of analyzing argumen- tation frameworks and their semantics based on an encoding into extensional type theory (classical higher-order logic). This representation enables the use of a wide range of interactive and automated higher-order reasoning tools for assessing argu- mentation frameworks. This includes the generation of labellings (and extensions), the assessment of meta-theoretic properties, the conduction of interactive empirical experiments, and the flexible analysis of argumentation frameworks with interpreted arguments.

The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical and legal theories at different conceptual layers. More concretely, it comprises, in form of a dataset (Isabelle/HOL theory files), formal encodings of multiple deontic logics, logic combinations, deontic paradoxes and normative theories in the higher-order proof assistant system Isabelle/HOL. The data were acquired through application of the LogiKEy methodology, which supports experimentation with different normative theories, in different application scenarios, and which is not tied to specific logics or logic combinations. Our workbench consolidates related research contributions of the authors and it may serve as a starting point for further studies and experiments in flexible and expressive ethical and legal reasoning. It may also support hands-on teaching of non-trivial logic formalisms in lecture courses and tutorials. The LogiKEy methodology and framework is discussed in more detail in the companion research article titled "Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support" [5].

A prototype for automated reasoning over legal texts, called NAI, is presented. As an input, NAI accepts formalized logical representations of such legal texts that can be created and curated using an integrated annotation interface. The prototype supports automated reasoning over the given text representation and multiple quality assurance procedures. The pragmatics of the NAI suite as well its feasibility in practical applications is studied on a fragment of the Smoking Prohibition (Children in Motor Vehicles) (Scotland) Act 2016 of the Scottish Parliament.

The annual meeting Deduktionstreffen is the prime activity of the Special Interest Group on Deduction Systems (FG DedSys) of the AI Section of the German Society for Informatics (GI-FBKI). It is a meeting with a familiar, friendly atmosphere, where everyone interested in deduction can report on their work in an informal setting.

A cooking application and a mechanical temperature controller based on the thermal expansion of sunflower oil were constructed and tested. Both components are parts of a solar cooking system, storing energy in an oil-based rock bed, made in the project work "Solar Heat Storage In Oil Based Rock Bed". This thesis is a part of a network project with universities in Mozambique, Uganda, Ethiopia and Tanzania, and focuses on energy supply to rural and off-grid communities in Africa. The motivation is to store energy from renewable energy sources, for later to be used in food preparations after sunset. Moreover, a simple system is desired, to make the operation and maintenance as easy as possible. This functional mechanical temperature controller will provide more flexibility to the solar cooking system, making it feasible for more settings than the system constructed in the project work. A mechanical temperature controller was made from two components; a piston actuator and a sliding valve. Three piston actuator designs were constructed and tested, all of which were connected to a closed pipe system with a copper coil filled with sunflower oil. The copper coil was submerged in a container holding sunflower oil and a heating element. During heating, the sunflower oil inside the copper coil expands due to the temperature change, giving a displacement of the piston actuator. The displacement is the motion which controls the sliding valve. Three sliding valve designs were constructed and tested, all utilising the linear motion from the piston actuator. The valve determines the flow direction, either towards the heat storage or for further heating, depending on the flow temperature. The valve can be used with and without circulation of the oil. Leaks caused problems throughout the production and tests of the components. A functional sliding valve was successfully constructed, whereas the first piston actuators were faulty due to leaks. The accuracy of the piston actuators made in the workshop at NTNU was not satisfying. Therefore, prefabricated pneumatic pistons were acquired. Preliminary tests gave promising results. Nevertheless, tests of the full system were not conducted due to the limited time. Two designs for a cooking application were made using a practical and a theoretical approach. The practical approach design was constructed and tested. The cooking effect was promising compared to other solar cookers, but it needs to be upscaled and further improved in order to deliver energy in the same order of magnitude as already established solar cookers. A test setup of the solar cooking system was made at Makerere University, Kampala, Uganda. The fill valve from the co-project was used as the temperature controller. Demonstrations proved the system made at NTNU is capable of being reproduced locally and is a concept suited for further development.

Dieser Beitrag diskutiert den Einsatz von interaktiven und automatischen Theorembeweisern in der universitären Lehre. Moderne Theorembeweiser scheinen geeignet zur Implementierung des dialogischen Lernens und als E-Assessment-Werkzeug in der Logikausbilding. Exemplarisch skizzieren wir ein innovaties Lehrprojekt zum Thema „Komputationale Metaphysik“, in dem die zuvor genannten Werkzeuge eingesetzt werden.

Church's Simple Theory of Types (STT), also referred to as classical higher-order logik, is an elegant and expressive formal system built on top of the simply typed λ-calculus. Its mechanisms of explicit binding and quantification over arbitrary sets and functions allow the representation of complex mathematical concepts and formulae in a concise and unambiguous manner. Higher-order automated theorem proving (ATP) has recently made major progress and several sophisticated ATP systems for higher-order logic have been developed, including Satallax, Osabelle/HOL and LEO-II. Still, higher-order theorem proving is not as mature as its first-order counterpart, and robust implementation techniques for efficient data structures are scarce. In this thesis, a higher-order term representation based upon the polymorphically typed λ-calculus is presented. This term representation employs spine notation, explicit substitutions and perfect term sharing for efficient term traversal, fast β-normalization and reuse of already constructed terms, respectively. An evaluation of the term representation is performed on the basis of a heterogeneous benchmark set. It shows that while the presented term data structure performs quite well in general, the normalization results indicate that a context dependent choice of reduction strategies is beneficial. A term indexing data structure for fast term retrieval based on various low-level criteria is presented and discussed. It supports symbol-based term retrieval, indexing of terms via structural properties, and subterm indexing.

This report presents a master thesis on 3D visualization for pre-operation planning of orthopedic surgery done for Sectra Medical Systems AB. The focus is on visualizing clinically relevant data for planning a Total Hip Replacement (THR). The thesis includes a pre-study and the implementation of a prototype using the Sectra IDS7 workstation.