Related papers: Polymorphism Meets DHOL
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with PVS being a notable…
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a…
The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its…
Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL.…
Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep…
Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to…
An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant…
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on…
A semantical embedding of input/output logic in classical higher-order logic is presented. This embedding enables the mechanisation and automation of reasoning tasks in input/output logic with off-the-shelf higher-order theorem provers and…
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.…
Large computer-understandable proofs consist of millions of intermediate logical steps. The vast majority of such steps originate from manually selected and manually guided heuristics applied to intermediate goals. So far, machine learning…
The Distributed Ontology Language (DOL) is currently being standardized within the OntoIOp (Ontology Integration and Interoperability) activity of ISO/TC 37/SC 3. It aims at providing a unified framework for (1) ontologies formalized in…
Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with…
This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the…
We discuss the syntax and semantics of relational Horn logic (RHL) and partial Horn logic (PHL). RHL is an extension of the Datalog programming language that allows introducing and equating variables in conclusions. PHL is a syntactic…
Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that handles realizability as a syntactic translation of propositions…
We explore the expressive power of HOL, a system of higher-order logic, and its relationship to the simply-typed lambda calculus and Church's simple theory of types, arguing for the potential of HOL as a unifying logical framework, capable…
Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for…
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's…
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an…