相关论文: Extending Nunchaku to Dependent Type Theory

We present a consequence-based calculus for concept subsumption and classification in the description logic ALCHOIQ, which extends ALC with role hierarchies, inverse roles, number restrictions, and nominals. By using standard…

This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such as Agda. The difference from prior works is that these…

Counterfactuals answer questions of what would have been observed under altered circumstances and can therefore offer valuable insights. Whereas the classical interventional interpretation of counterfactuals has been studied extensively,…

We present an approach to develop folds for nested data types using dependent types. We call such folds $\textit{dependently typed folds}$, they have the following properties. (1) Dependently typed folds are defined by well-founded…

The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type theory or cubical type theory. This article describes these…

In a previous work, we proved that an important part of the Calculus of Inductive Constructions (CIC), the basis of the Coq proof assistant, can be seen as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of…

Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the…

This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways…

Draco introduced a constraint-based framework to model visualization design in an extensible and testable form. It provides a way to abstract design guidelines from theoretical and empirical studies and applies the knowledge in automated…

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.…

A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely…

The formal construction of the second-order logic or predicate calculus essentially adds quantifiers to propositional logic. Why second-order logic cannot be reduced to that of the first order? How to demonstrate that certain predicates are…

First-order logic, and quantifiers in particular, are widely used in deductive verification. Quantifiers are essential for describing systems with unbounded domains, but prove difficult for automated solvers. Significant effort has been…

Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run.…

This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language,…

The full power of human language-based communication cannot be realized without negation. All human languages have some form of negation. Despite this, negation remains a challenging phenomenon for current natural language understanding…

We give an overview of some developments in dependence and independence logic. This is a tiny selection, intended for a newcomer, from a rapidly growing literature on the topic. Furthermore, we discuss conditional independence atoms and we…

A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists; greatest fixedpoints express coinductive…

Testing for pairwise independence for the case where the number of variables may be of the same size or even larger than the sample size has received increasing attention in the recent years. We contribute to this branch of the literature…

Hammers are tools that provide general purpose automation for formal proof assistants. Despite the gaining popularity of the more advanced versions of type theory, there are no hammers for such systems. We present an extension of the…