Related papers: Automated Theorem Proving for Prolog Verification

Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing…

Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving. In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called…

Growing renewable penetration introduces substantial uncertainty into power system operations, necessitating frequent adaptation of dispatch objectives and constraints and challenging expertise-intensive, near-real-time modeling workflows.…

PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reasoner invocations and…

We develop combinatorial test generation algorithms for progressively more powerful theorem provers, covering formula languages ranging from the implicational fragment of intuitionistic logic to full intuitionistic propositional logic. Our…

Formal verification provides a rigorous and systematic approach to ensure the correctness and reliability of software systems. Yet, constructing specifications for the full proof relies on domain expertise and non-trivial manpower. In view…

Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static verifier. In this work we use metaprogramming to generate code…

Uncertain information is being taken into account in an increasing number of application fields. In the meantime, abduction has been proved a powerful tool for handling hypothetical reasoning and incomplete knowledge. Probabilistic logical…

Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration of automated theorem provers in a pure and simple setting.…

The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus allowing for external evidence and for postponing,…

Higher-order constructs extend the expressiveness of first-order (Constraint) Logic Programming ((C)LP) both syntactically and semantically. At the same time assertions have been in use for some time in (C)LP systems helping programmers…

The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes…

We propose relational linear programming, a simple framework for combing linear programs (LPs) and logic programs. A relational linear program (RLP) is a declarative LP template defining the objective and the constraints through the logical…

To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former…

Intrinsic self-correct was a method that instructed large language models (LLMs) to verify and correct their responses without external feedback. Unfortunately, the study concluded that the LLMs could not self-correct reasoning yet. We find…

First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed systems. However, specifying many natural objects, such as a ring…

This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of…

A recent trend in object oriented (OO) programming languages is the use of Access Permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how…

We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. To address this…

Despite recent advances in modern machine learning algorithms, the opaqueness of their underlying mechanisms continues to be an obstacle in adoption. To instill confidence and trust in artificial intelligence systems, Explainable Artificial…