The addition of bounded quantification and partial functions to a computational logic and its theorem prover

We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects in the logic, to define an interpreter for such expressions as a function in the logic, and then define quantifiers as ‘mapping functions’. The novelty of our approach lies in the formalization of the interpreter and its interaction with the underlying logic. Our method has several advantages over other formal systems that provide quantifiers and partial functions in a logical setting. The most important advantage is that proofs not involving quantification or partial recursive functions are not complicated by such notions as ‘capturing’, ‘bottom’, or ‘continuity’. Naturally enough, our formalization of the partial functions is nonconstructive. The theorem prover for the logic has been modified to support these new features. We describe the modifications. The system has proved many theorems that could not previously be stated in our logic. Among them are:

? classic quantifier manipulation theorems, such as $$\sum\limits_{{\text{l}} = 0}^{\text{n}} {{\text{g}}({\text{l}}) + {\text{h(l) = }}} \sum\limits_{{\text{l = }}0}^{\text{n}} {{\text{g}}({\text{l}})} + \sum\limits_{{\text{l = }}0}^{\text{n}} {{\text{h(l)}};} $$

? elementary theorems involving quantifiers, such as the Binomial Theorem: $$(a + b)^{\text{n}} = \sum\limits_{{\text{l = }}0}^{\text{n}} {\left( {_{\text{i}}^{\text{n}} } \right)} \user2{ }{\text{a}}^{\text{l}} {\text{b}}^{{\text{n - l}}} ;$$

? elementary theorems about ‘mapping functions’ such as: $$(FOLDR\user2{ }'PLUS\user2{ O L) = }\sum\limits_{{\text{i}} \in {\text{L}}}^{} {{\text{i}};} $$

? termination properties of many partial recursive functions such as the fact that an application of the partial function described by $$\begin{gathered} (LEN X) \hfill \\ \Leftarrow \hfill \\ ({\rm I}F ({\rm E}QUAL X NIL) \hfill \\ {\rm O} \hfill \\ (ADD1 (LEN (CDR X)))) \hfill \\ \end{gathered} $$ terminates if and only if the argument ends in NIL;

? theorems about functions satisfying unusual recurrence equations such as the 91-function and the following list reverse function: $$\begin{gathered} (RV X) \hfill \\ \Leftarrow \hfill \\ ({\rm I}F (AND (LISTP X) (LISTP (CDR X))) \hfill \\ (CONS (CAR (RV (CDR X))) \hfill \\ (RV (CONS (CAR X) \hfill \\ (RV (CDR (RV (CDR X))))))) \hfill \\ X). \hfill \\ \end{gathered} $$

     

Successive overrelaxation method with projection for finite element solutions applied to the Dirichlet problem of the nonlinear elliptic equation Δu-bu2

this study is a continuation of a previous paper [Computing 38 (1987), pp.117–132]. In this paper, we consider the successive overrelaxation method with projection for obtaining finite element solutions applied to the Dirichlet problem of the nonlinear elliptic equation $$\begin{gathered} \Delta u = bu^2 in\Omega , \hfill \\ u = g(x)on\Gamma . \hfill \\ \end{gathered} $$ . Some numerical examples are given to illustrate the effectiveness.     

Convergence,stability and truncation error estimation of a method for the numerical integration of the initial value problemY″=F(X,Y)

In this paper a detailed study of the convergence and stability of a numerical method for the differential problem $$\left\{ \begin{gathered} y'' = f(x,y) \hfill \\ y(x_0 ) = y_0 \hfill \\ y'(x_0 ) = y_0 ^\prime \hfill \\ \end{gathered} \right.$$ has carried out and its truncation error estimated. Some numerical experiments are described.     

Formule di quadratura «chiuse» di tipo gaussiano: Tabulzione dei nodi e dei coefficienti

The coefficientsA _hi and the nodesx _mi for «closed” Gaussian-type quadrature formulae $$\int\limits_{ - 1}^1 {f(x)dx = \sum\limits_{h = 0}^{2_8 } {\sum\limits_{i = 0}^{m + 1} {A_{hi} f^{(h)} (x_{mi} ) + R\left[ {f(x)} \right]} } } $$ withx _m0 =?1,x _{m, m+1} =1 andR[f(x)]=0 iff(x) is a polinomial of degree at most2m(s+1)+2(2s+1)?1, have been tabulated for the cases: $$\left\{ \begin{gathered} s = 1,2 \hfill \\ m = 2,3,4,5 \hfill \\ \end{gathered} \right.$$ .     

Resolution numerique de quelques problemes raides en mecanique des milieux faiblement compressibles

This paper deals with the numerical approximation of some «stiff» problems by asymptotic expansion of the solution. The model problem is the stationary linearized equation of slightly compressible fluids: $$\begin{gathered} \ll Find u_\varepsilon \varepsilon \left[ {H_0^1 (\Omega )} \right]^n s.t. \hfill \\ - \mu \Delta u_\varepsilon - \frac{1}{\varepsilon } grad div u_\varepsilon = f in \Omega \gg \hfill \\ \end{gathered} $$ where ∈ is asmall parameter; numerical treatment of the problem is thus difficult («stiff» problem). We establish existence and unicity of an asymptotic expansion foru, and use it to computeu. In the usual cases, with small divergence, the numerical results are far better than those obtained by direct discretisation of the problem. We also construct asymptotic expansions for the solutions of some nonlinear or non-stationary related problems.     

Esistenza,unicità e calcolo della soluzione di un sistema non lineare

LetX be a point of the realn-dimensional Euclidean space ? ⁿ ,G(X) a given vector withn real components defined in ? ^u ,U an unknown vector withs real components,K a known vector withs real components andA a given reals×n matrix of ranks. Assuming that, for every pair of pointsX ₁ , X₂of ? ⁿ ,G(X) satisfies the conditions $$(G(X_1 ) - G(X_2 ), X_1 - X_2 ) \geqslant o (X_1 - X_2 , X_1 - X_2 )$$ and $$\left\| {(G(X_1 ) - G(X_2 )\left\| { \leqslant M} \right\|X_1 - X_2 )} \right\|$$ wherec andM are positive constants, we prove that a unique solution of the system $$\left\{ \begin{gathered} G(X) + A ^T U = 0 \hfill \\ AX = K \hfill \\ \end{gathered} \right.$$ exists and we show a method for finding such a solution     

Sul calcolo numerico della soluzione di un problema ai limiti per l’equazione differenzialey′=f(x,y,λ)

In this paper the Author gives a method of solving numerically the problem:

$$\begin{gathered} y'_\lambda (x) = f(x,y_\lambda (x),\lambda ) \hfill \\ y_\lambda (x) = y_1 ,y_\lambda (x_2 ) = y_2 \hfill \\ \end{gathered} $$     

A note on the Bernstein algorithm for bounds for interval polynomials

In computing the range of values of a polynomial over an intervala≤x≤b one may use polynomials of the form $$\left( {\begin{array}{*{20}c} k \\ j \\ \end{array} } \right)\left( {x - a} \right)^j \left( {b - x} \right)^{k - j} $$ called Bernstein polynomials of the degreek. An arbitrary polynomial of degreen may be written as a linear combination of Bernstein polynomials of degreek≥n. The coefficients of this linear combination furnish an upper/lower bound for the range of the polynomial. In this paper a finite differencelike scheme is investigated for this computation. The scheme is then generalized to interval polynomials.     

Soluzione delle equazioni della cinetica di un reattore nucleare per mezzo di approssimazioni successive di tipo monotono

The solution of the one-energy group space-independent reactor kinetics equations is obtained in the form of the limit of two monotone bounded sequences of functions {N _j ^?} and {N _j ⁺}, non decreasing and non increasing respectively, defined as $$\begin{gathered} N_{j + 1}^ - = T_1 N_j^ + + T_2 N_j^ - + f \hfill \\ N_{j + 1}^ + = T_1 N_j^ - + T_2 N_j^ + + f \hfill \\ \end{gathered} $$ whereT ₁ andT ₂ are monotone-type operators, precisely antitone and isotone. In this work a procedure for obtaining the two initial elements,N ₀ ^? andN ₀ ⁺, satisfying the required properties to assure the convergence of the two sequences {N _j ^?} and {N _j ⁺}, is described; moreover, it is proved that the two sequences converge uniformely to the same limit. In addition, some numerical results are presented.     

Un metodo del terzo ordine per l'integrazione numerica dell'equazione differenziale ordinaria

For the numerical integration of the ordinary differential equation $$\frac{{dy}}{{dx}} = F(x,y) y(x_0 ) = y_0 \begin{array}{*{20}c} x \\ {x_0 } \\ \end{array} \varepsilon [a,b]$$ a third method utilizing only two points for every step, is determined different from the analogous Runge-Kutta method employing three points; it is useless take the first step as the «pseudo Runge-Kutta method». The truncation error is given, the convergence is proved and finally a numerical exercise is given.     

Metodi Multistep con accelerazione per la risoluzione numerica dei sistemi di equazioni differenziali ordinarie

In this paper a procedure for the acceleration of the convergence is given. It allows the doubling of the order of the multistep methods for the numerical solution of the systems of ordinary differential equations: $$Y' = F(x,Y); Y_0 = Y(x_0 ) \begin{array}{*{20}c} x \\ {x_0 } \\ \end{array} \in [a,b]$$ whereY andF(x,Y) aret-vectors.     

The structure of nonsingular polynomial matrices

LetK be a field and letL ∈ K ^{n × n [z]} be nonsingular. The matrixL can be decomposed as \(L(z) = \hat Q(z)(Rz + S)\hat P(z)\) so that the finite and (suitably defined) infinite elementary divisors ofL are the same as those ofRz + S, and \(\hat Q(z)\) and \(\hat P(z)^T\) are polynomial matrices which have a constant right inverse. If $$Rz + S = \left( {\begin{array}{*{20}c} {zI - A} & 0 \\ 0 & {I - zN} \\ \end{array} } \right)$$ andK is algebraically closed, then the columns of \(\hat Q\) and \(\hat P^T\) consist of eigenvectors and generalized eigenvectors of shift operators associated withL.     

Richardson Extrapolation on Some Recent Numerical Quadrature Formulas for Singular and Hypersingular Integrals and Its Study of Stability

Recently, we derived some new numerical quadrature formulas of trapezoidal rule type for the integrals \(I^{(1)}[g]=\int ^b_a \frac{g(x)}{x-t}\,dx\) and \(I^{(2)}[g]=\int ^b_a \frac{g(x)}{(x-t)^2}\,dx\) . These integrals are not defined in the regular sense; \(I^{(1)}[g]\) is defined in the sense of Cauchy Principal Value while \(I^{(2)}[g]\) is defined in the sense of Hadamard Finite Part. With \(h=(b-a)/n, \,n=1,2,\ldots \) , and \(t=a+kh\) for some \(k\in \{1,\ldots ,n-1\}, \,t\) being fixed, the numerical quadrature formulas \({Q}^{(1)}_n[g]\) for \(I^{(1)}[g]\) and \(Q^{(2)}_n[g]\) for \(I^{(2)}[g]\) are $$\begin{aligned} {Q}^{(1)}_n[g]=h\sum ^n_{j=1}f(a+jh-h/2),\quad f(x)=\frac{g(x)}{x-t}, \end{aligned}$$ and $$\begin{aligned} Q^{(2)}_n[g]=h\sum ^n_{j=1}f(a+jh-h/2)-\pi ^2g(t)h^{-1},\quad f(x)=\frac{g(x)}{(x-t)^2}. \end{aligned}$$ We provided a complete analysis of the errors in these formulas under the assumption that \(g\in C^\infty [a,b]\) . We actually show that $$\begin{aligned} I^{(k)}[g]-{Q}^{(k)}_n[g]\sim \sum ^\infty _{i=1} c^{(k)}_ih^{2i}\quad \text {as}\,n \rightarrow \infty , \end{aligned}$$ the constants \(c^{(k)}_i\) being independent of \(h\) . In this work, we apply the Richardson extrapolation to \({Q}^{(k)}_n[g]\) to obtain approximations of very high accuracy to \(I^{(k)}[g]\) . We also give a thorough analysis of convergence and numerical stability (in finite-precision arithmetic) for them. In our study of stability, we show that errors committed when computing the function \(g(x)\) , which form the main source of errors in the rest of the computation, propagate in a relatively mild fashion into the extrapolation table, and we quantify their rate of propagation. We confirm our conclusions via numerical examples.     

Rounds in Combinatorial Search

A set system $\mathcal{H} \subseteq2^{[m]}$ is said to be separating if for every pair of distinct elements x,y∈[m] there exists a set $H\in\mathcal{H}$ such that H contains exactly one of them. The search complexity of a separating system $\mathcal{H} \subseteq 2^{[m]}$ is the minimum number of questions of type “x∈H?” (where $H \in\mathcal{H}$ ) needed in the worst case to determine a hidden element x∈[m]. If we receive the answer before asking a new question then we speak of the adaptive complexity, denoted by $\mathrm{c} (\mathcal{H})$ ; if the questions are all fixed beforehand then we speak of the non-adaptive complexity, denoted by $\mathrm{c}_{na} (\mathcal{H})$ . If we are allowed to ask the questions in at most k rounds then we speak of the k-round complexity of $\mathcal{H}$ , denoted by $\mathrm{c}_{k} (\mathcal{H})$ . It is clear that $|\mathcal{H}| \geq\mathrm{c}_{na} (\mathcal{H}) = \mathrm{c}_{1} (\mathcal{H}) \geq\mathrm{c}_{2} (\mathcal{H}) \geq\cdots\geq\mathrm{c}_{m} (\mathcal{H}) = \mathrm{c} (\mathcal{H})$ . A group of problems raised by G.O.H. Katona is to characterize those separating systems for which some of these inequalities are tight. In this paper we are discussing set systems $\mathcal{H}$ with the property $|\mathcal{H}| = \mathrm{c}_{k} (\mathcal{H}) $ for any k≥3. We give a necessary condition for this property by proving a theorem about traces of hypergraphs which also has its own interest.     

A technical note on AC-Unification. The number of minimal unifiers of the equation αx1 + ⋯ + αxp ≐AC βy1 + ⋯ + βyq

We show in this note that the equation αx₁ + #x22EF; +αx_p?_ACβy₁ + α +βy_q where + is an AC operator and αx stands for x+...+x (α times), has exactly $$\left( { - 1} \right)^{p + q} \sum\limits_{i = 0}^p {\sum\limits_{j = 0}^q {\left( { - 1} \right)^{1 + 1} \left( {\begin{array}{*{20}c} p \\ i \\ \end{array} } \right)\left( {\begin{array}{*{20}c} q \\ j \\ \end{array} } \right)} 2^{\left( {\alpha + \begin{array}{*{20}c} {j - 1} \\ \alpha \\ \end{array} } \right)\left( {\beta + \begin{array}{*{20}c} {i - 1} \\ \beta \\ \end{array} } \right)} } $$ minimal unifiers if gcd(α, β)=1.     

Metodi pseudo Runge-Kutta ottimali

For the numerical integration of the problem with initial value $$y' = f(x,y),y(x_0 ) = y_0 ,\begin{array}{*{20}c} {\begin{array}{*{20}c} x \\ {x_0 } \\ \end{array} \in [a,b],} \\ \end{array} $$ the pseudo R. K. methods of second kind are taken again and approximations are drawn, that in particular casef(x, y)≡f(x) are reduced to quadrature formulae of Radau and Lobatto. The limits of the trancation's error and the stability's intervals of the pseudo R. K. methods of the first and second species with the approximations of the same order of R. K. are determined and compared. At the end of that, a numerical example is taken.     

On the computation of Tricomi's ψ function

Two methods for calculating Tricomi's confluent hypergeometric function are discussed. Both methods are based on recurrence relations. The first method converges like $$\exp ( - \alpha |\lambda |^{1/3} n^{2/3} )for some \alpha > 0$$ and the second like $$\exp ( - \beta |\lambda |^{1/2} n^{1/2} )for some \beta > 0.$$ Several examples are presented.     

Quantitative theorems on approximation by Bernstein-Stancu operators

In 1972 D. D. Stancu introduced a generalization \(L_{mp} ^{< \alpha \beta \gamma > }\) of the classical Bernstein operators given by the formula $$L_{mp}< \alpha \beta \gamma > (f,x) = \sum\limits_{k = 0}^{m + p} {\left( {\begin{array}{*{20}c} {m + p} \\ k \\ \end{array} } \right)} \frac{{x^{(k, - \alpha )} \cdot (1 - x)^{(m + p - k, - \alpha )} }}{{1^{(m + p, - \alpha )} }}f\left( {\frac{{k + \beta }}{{m + \gamma }}} \right)$$ . Special cases of these operators had been investigated before by quite a number of authors and have been under investigation since then. The aim of the present paper is to prove general results for all positiveL _mp ^<αβγ> 's as far as direct theorems involving different kinds of moduli of continuity are concerned. When applied to special cases considered previously, all our corollaries of the general theorems will be as good as or yield improvements of the known results. All estimates involving the second order modulus of continuity are new.     

A Unified Approach to Approximating Partial Covering Problems

An instance of the generalized partial cover problem consists of a ground set U and a family of subsets ${\mathcal{S}}\subseteq 2^{U}$ . Each element e??U is associated with a profit p(e), whereas each subset $S\in \mathcal{S}$ has a cost c(S). The objective is to find a minimum cost subcollection $\mathcal{S}'\subseteq \mathcal{S}$ such that the combined profit of the elements covered by $\mathcal{S}'$ is at least P, a specified profit bound. In the prize-collecting version of this problem, there is no strict requirement to cover any element; however, if the subsets we pick leave an element e??U uncovered, we incur a penalty of ??(e). The goal is to identify a subcollection $\mathcal{S}'\subseteq \mathcal{S}$ that minimizes the cost of $\mathcal{S}'$ plus the penalties of uncovered elements. Although problem-specific connections between the partial cover and the prize-collecting variants of a given covering problem have been explored and exploited, a more general connection remained open. The main contribution of this paper is to establish a formal relationship between these two variants. As a result, we present a unified framework for approximating problems that can be formulated or interpreted as special cases of generalized partial cover. We demonstrate the applicability of our method on a diverse collection of covering problems, for some of which we obtain the first non-trivial approximability results.     

Sulle formule di quadratura di Tschebyscheff

For the Tschebyscheff quadrature formula: $$\int\limits_{ - 1}^1 {\left( {1 - x^2 } \right)^{\lambda - 1/2} f(x) dx} = K_n \sum\limits_{k = 1}^n {f(x_{n,k} )} + R_n (f), \lambda > 0$$ it is shown that the degre,N, of exactness is bounded by: $$N \leqslant C(\lambda )n^{1/(2\lambda + 1)} $$ whereC(λ) is a convenient function of λ. For λ=1 the complete solution of Tschebyscheff's problem is given.