scholarly journals Progress in Automating Higher-Order Ontology Reasoning

10.29007/dtnz ◽  
2018 ◽  
Author(s):  
Christoph Benzmüller ◽  
Adam Pease
Keyword(s):  
Automated Theorem Proving ◽  
Knowledge Engineering ◽  
Higher Order ◽  
Theorem Prover ◽  
Ontology Reasoning ◽  
Order Form ◽  
Form Representation ◽  
Engineering Environment ◽  
Representation Language ◽  
Upper Level

We report on the application of higher-order automated theorem proving in ontology reasoning. Concretely, we have integrated the Sigma knowledge engineering environment and the Suggested Upper-Level Ontology SUMO with the higher-order theorem prover LEO-II. The basis for this integration is a translation from SUMO representations into the new typed higher-order form representation language TPTP THF. We illustrate the benefits of our integration with examples, report on experiments and analyze open challenges.

scholarly journals Automated Higher-order Reasoning about Quantales

10.29007/l2sz ◽  
2018 ◽  
Author(s):  
Han-Hing Dang ◽  
Peter Höfner
Keyword(s):  
Quantum Mechanics ◽  
Automated Theorem Proving ◽  
Higher Order ◽  
Order Logic ◽  
Theorem Prover ◽  
Higher Order Logic ◽  
Order Form ◽  
Problem Library ◽  
Practical Experiences ◽  
To Receive

Originally developed as an algebraic characterisation for quantum mechanics, the algebraic structure of quantales nowadays finds widespread applications ranging from (non-commutative) logics to hybrid systems. We present an approach to bring reasoning about quantales into the realm of (fully) automated theorem proving. This will yield automation in various (new) fields of applications in the future. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Problem Library for higher-order logic. In particular, we give an encoding of quantales in the typed higher-order form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.

scholarly journals Understanding LEO-II’s proofs

10.29007/x9c9 ◽  
2018 ◽  
Author(s):  
Nik Sultana ◽  
Christoph Benzmüller
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Higher Order ◽  
Target Audience ◽  
Theorem Prover ◽  
First Order

The LEO and LEO-II provers have pioneered the integration of higher-order and first-order automated theorem proving. To date, the LEO-II system is, to our knowledge, the only automated higher-order theorem prover which is capable of generating joint higher-order–first-order proof objects in TPTP format. This paper discusses LEO-II’s proof objects. The target audience are practitioners with an interest in using LEO-II proofs within other systems.

scholarly journals Invariants and Robustness of BIP Models

10.29007/prxp ◽  
2018 ◽  
Author(s):  
Jan Olaf Blech ◽  
Thanh-Hung Nguyen ◽  
Michael Perin
Keyword(s):  
Embedded Systems ◽  
Higher Order ◽  
Theorem Prover ◽  
Important Goal ◽  
Invariant Generation ◽  
Execution Traces ◽  
Verification Tool ◽  
Verification Tools ◽  
Generation Mechanisms ◽  
Natural Way

In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.

Planning meets verification and validation in a knowledge engineering environment

2014 ◽  
Vol 8 (1) ◽  
pp. 87-100 ◽  
Author(s):  
Andrea Orlandini ◽  
Giulio Bernardi ◽  
Amedeo Cesta ◽  
Alberto Finzi
Keyword(s):  
Knowledge Engineering ◽  
Verification And Validation ◽  
Engineering Environment

The ART (Activities, Resources, Technological Supports) in On-Site and Online Learning, and Students’ Perceptions of Acquisition of Thinking and Team-Building Skills

2012 ◽  
pp. 287-304
Author(s):  
Jennifer D.E. Thomas ◽  
Danielle Morin
Keyword(s):  
Online Learning ◽  
Team Building ◽  
Strong Support ◽  
Higher Order Thinking ◽  
Thinking Skills ◽  
Higher Order ◽  
Online Resources ◽  
Higher Order Thinking Skills ◽  
Upper Level ◽  
Art Activities

The efficacy of different modes of instruction delivery, whether on-site, online, or a combination, continues to be debated in academic circles. This chapter takes a somewhat different view from most other research and compares students’ perceptions of support provided in the acquisition of various thinking and team-building skills, as a consequence of the integration of various activities, resources, and technologies (ART) used in an upper level Distributed Computing (DC) course. The findings indicate that students perceived strong support for their acquisition of higher-order thinking skills (HOTS) and team-building skills (TBS) from the offline resources, but moderate support from the online resources and technologies provided in the course, which was in opposition to the grades received. A deeper analysis of the results pointed, among other things, to the use of cases as being most supportive of the acquisition of the higher-order thinking skills and of team-building skills.

Looking for Information-Literate Thinking in Undergraduate Subject Searching

2013 ◽  
Author(s):  
Rumi Y. Graham
Keyword(s):  
Multiple Case Study ◽  
Higher Order ◽  
Order Information ◽  
Domain Experts ◽  
Academic Subject ◽  
Premier Cycle ◽  
Multiple Case ◽  
Upper Level ◽  
Premier Cycle Universitaire

To what extent do upper-level, academically outstanding undergraduates employ the kind of higher-order information literate thinking during subject searching commonly associated with search and domain experts? This paper reports on a multiple case study exploration of this question involving eight students and their genuine academic subject searches over a school year.Dans quelle mesure les étudiants de premier cycle universitaire aux meilleurs résultats académiques emploient-ils des techniques de littératie de haut niveau communément trouvées chez les experts lors de recherches par sujet? Cette communication présente les résultats de huit études de cas menées auprès d’étudiants suivis pendant leur cheminement scolaire au cours d’une année. 

Sign in / Sign up

Export Citation Format

Share Document