Towards String Support in JayHorn (Competition Contribution)

Abstractis a Horn clause-based model checker for Java programs that has been competing at SV-COMP since 2019. An ongoing research and implementation effort is to add support for data-type to . Since current Horn solvers do not support strings natively, we consider a representation of (unbounded) strings using algebraic data-types, more precisely as lists. This paper discusses Horn clause encodings of different string operations, and presents preliminary results.

The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen’s classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

Horn Clause Techniques in Rehabilitation Clinic for Return to Work

Rehabilitation therapy aims to enable disabled patients to maintain optimal functioning upon achieving returnto-work (RTW) approval. The Berg Balance Scale (BBS) is a benchmark for activity accomplishment featured in the International Classification of Functioning, Disability and Health Framework (ICF). The ICF is used by physiotherapist (PT) and occupational therapist (OT) to determine the functional mobility of disabled patient. Conventionally, practitioners measure, record, and analyze assessment results manually which resulting in difficulty in predicting patient progression. The large data volume involved in the RTW process requires synthesize and reasoning for decision making purposes. Thus, there is a need to identify an efficient reasoning technique to facilitate the decision making process. This study highlights the use of Horn Clause in decision tree to assist medical doctor in assessing improvement of RTW approved patient based on the BBS assessment. The Horn Clause is one of the fundamental reasoning techniques applied in various domains including healthcare. The next phase of this study is to test the efficiency of the Horn Clause reasoning based on patient’s stroke recovery and spinal cord injury.

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis

First-order resolution has been used for type inference for many years, including in Hindley-Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method.

Tree dimension in verification of constrained Horn clauses

In this paper, we show how the notion of tree dimension can be used in the verification of constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCsP, we define a transformation ofPyielding adimension-boundedset of CHCsP≤k. The set of derivations forP≤kconsists of the derivations forPthat have dimension at mostk. We also show how to construct a set of clauses denotedP>kwhose derivations have dimension exceedingk. We then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results.