Search
Search Results
-
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search...
-
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting
We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms’ performance...
-
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic
In recent years some papers have addressed the problem of the validity in Intuitionistic Propositional Logic (IPL) using the approach proposed by...
-
Gale-Shapley Verified
This paper presents a detailed verification of the Gale-Shapley algorithm for stable matching (or marriage). The verification proceeds by stepwise...
-
Automated Generation of Geometry Proof Problems Based on Point Geometry Identity
The automated generation of geometry proof problems represents a burgeoning research domain in the realm of artificial intelligence, with significant...
-
Formalized Functional Analysis with Semilinear Maps
Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such...
-
Linear Resources in Isabelle/HOL
We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of...
-
Sequent Calculi for Choice Logics
Choice logics constitute a family of propositional logics and are used for the representation of preferences, with especially qualitative choice logic ...
-
Schematic Program Proofs with Abstract Execution
We propose Abstract Execution , a static verification framework based on symbolic execution and dynamic frames for proving properties of schematic ...
-
-
Should Decisions in QCDCL Follow Prefix Order?
Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the...
-
Non-termination in Term Rewriting and Logic Programming
In this paper, we define two particular forms of non-termination, namely loops and binary chains , in an abstract framework that encompasses term...
-
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
We present an automatic theorem prover for projective incidence geometry. This prover does not consider coordinates. Instead, it follows a...
-
Programming-Based Formal Languages and Automata Theory Design, Implement, Validate, and Prove
This textbook introduces formal languages and automata theory for upper-level undergraduate or beginning graduate students. While it contains the...
-
Human and Artificial Rationalities Second International Conference, HAR 2023, Paris, France, September 19–22, 2023, Proceedings
This book constitutes the proceedings of the Second International Conference on Human and Artificial Rationalities, HAR 2023, which took place in...
-
Foundations of Information and Knowledge Systems 13th International Symposium, FoIKS 2024, Sheffield, UK, April 8–11, 2024, Proceedings
This LNCS conference volume constitutes the proceedings of the 13th International Symposium, FoIKS 2024, in Sheffield, UK, in April 2024. The 18 full...
-
Rigorous State-Based Methods 10th International Conference, ABZ 2024, Bergamo, Italy, June 25–28, 2024, Proceedings
This book constitutes the refereed proceedings of the 10th International Conference on Rigorous State-Based Methods, ABZ 2024, held in Bergamo,...
-
Some Remarks About Dependent Type Theory
The goal of this chapter is to describe a calculus designed in 1984/1985. This calculus was obtained by applying the ideas introduced by N.G. de...
-
On Identifiability of BN2A Networks
In this paper, we consider two-layer Bayesian networks. The first layer consists of hidden (unobservable) variables and the second layer consists of...
-
Hypergraphs in Logic Programming
Heterogeneous data is a significant topic in today’s context, necessitating the development of AI tools. Logic programming is a powerful approach for...