Related papers: On Modular Termination Proofs of General Logic Pro…
Every definite logic program has as its meaning a least Herbrand model with respect to the program-independent ordering "set-inclusion". In the case of normal logic programs there do not exist least models in general. However, according to…
We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By…
We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This…
Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where…
We consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear…
Determining whether a program terminates is a core challenge in program analysis with direct implications for correctness, verification, and security. We investigate whether transformer architectures can recognise termination patterns…
In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of…
Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete…
$\{log\}$ is a programming language at the intersection of Constraint Logic Programming, set programming and declarative programming. But $\{log\}$ is also a satisfiability solver for a theory of finite sets and finite binary relations.…
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed. However, so far all of them have been monolithic, i.e., a…
GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with…
Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate…
We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping…
We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded…
Scientists form hypotheses and experimentally test them. If a hypothesis fails (is refuted), scientists try to explain the failure to eliminate other hypotheses. The more precise the failure analysis the more hypotheses can be eliminated.…
The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual…
In considering the reliability of numerical programs, it is normal to "limit our study to the semantics dealing with numerical precision" (Martel, 2005). On the other hand, there is a great deal of work on the reliability of programs that…
We introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the…
Many logic programming based approaches can be used to describe and solve combinatorial search problems. On the one hand there is constraint logic programming which computes a solution as an answer substitution to a query containing the…
The general setting of this work is the constraint-based synthesis of termination arguments. We consider a restricted class of programs called lasso programs. The termination argument for a lasso program is a pair of a ranking function and…