A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo

Synchronizing Constrained Horn Clauses

10.29007/gr5c ◽

2018 ◽

Cited By ~ 3

Author(s):

Dmitry Mordvinov ◽

Grigory Fedyukovich

Keyword(s):

Iterative Algorithm ◽

Recurrence Relations ◽

Multiple Recurrence ◽

Integer Arithmetic ◽

Horn Clauses ◽

Constraint Language ◽

Non Linear

Simultaneous occurrences of multiple recurrence relations in a system of non-linear constrained Horn clauses are crucial for proving its satis ability. A solution of such system is often inexpressible in the constraint language. We propose to synchronize recurrent computations, thus increasing the chances for a solution to be found. We introduce a notion of CHC product allowing to formulate a lightweight iterative algorithm of merging recurrent computations into groups and prove its soundness. The evaluation over a set of systems handling lists and linear integer arithmetic confirms that the transformed systems are drastically more simple to solve than the original ones.

Download Full-text

B. The Non-Linear Calculations for Pulsating Stars

Symposium - International Astronomical Union ◽

10.1017/s0074180900019008 ◽

1967 ◽

Vol 28 ◽

pp. 105-176

Author(s):

Robert F. Christy

Keyword(s):

Major Part ◽

Afternoon Session ◽

Discussion Session ◽

Pulsating Stars ◽

Fourth Symposium ◽

Non Linear ◽

Considerable Discussion ◽

Informal Approach ◽

Preceding Session

(Ed. note: The custom in these Symposia has been to have a summary-introductory presentation which lasts about 1 to 1.5 hours, during which discussion from the floor is minor and usually directed at technical clarification. The remainder of the session is then devoted to discussion of the whole subject, oriented around the summary-introduction. The preceding session, I-A, at Nice, followed this pattern. Christy suggested that we might experiment in his presentation with a much more informal approach, allowing considerable discussion of the points raised in the summary-introduction during its presentation, with perhaps the entire morning spent in this way, reserving the afternoon session for discussion only. At Varenna, in the Fourth Symposium, several of the summaryintroductory papers presented from the astronomical viewpoint had been so full of concepts unfamiliar to a number of the aerodynamicists-physicists present, that a major part of the following discussion session had been devoted to simply clarifying concepts and then repeating a considerable amount of what had been summarized. So, always looking for alternatives which help to increase the understanding between the different disciplines by introducing clarification of concept as expeditiously as possible, we tried Christy's suggestion. Thus you will find the pattern of the following different from that in session I-A. I am much indebted to Christy for extensive collaboration in editing the resulting combined presentation and discussion. As always, however, I have taken upon myself the responsibility for the final editing, and so all shortcomings are on my head.)

Download Full-text