Center for Mathematics, Fundamental Applications and Operations Research

Funder

Organizational Unit

Publications

On the use of quasi-equidistant source points over the sphere surface for the method of fundamental solutions

Publication . Araújo, António; Serranho, Pedro

The method of fundamental solutions is broadly used in science and engineering to numerically solve the direct time-harmonic scattering problem. In 2D the choice of source points is usually made by considering an inner pseudo-boundary over which equidistant source points are placed. In 3D, however, this problem is much more challenging, since, in general, equidistant points over a closed surface do not exist. In this paper we discuss a method to obtain a quasi-equidistant point distribution over the unit sphere surface, giving rise to a Delaunay triangulation that might also be used for other boundary element methods. We give theoretical estimates for the expected distance between points and the expect area of each triangle. We illustrate the feasibility of the proposed method in terms of the comparison with the expected values for distance and area. We also provide numerical evidence that this point distribution leads to a good conditioning of the linear system associated with the direct scattering problem, being therefore an adequated choice of source points for the method of fundamental solutions.

2019Journal article

Open access

The Russell-Prawitz embedding and the atomization of universal instantiation

Publication . Espírito Santo, José; Ferreira, Gilda

Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system Fat, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain “dinaturality” conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system Fat; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into Fat does not.

2020Journal article

Open access

An infinite dimensional umbral calculus

Publication . Oliveira, Maria João

2018-01-02Conference object

Restricted access

A refined interpretation of intuitionistic logic by means of atomic polymorphism

Publication . Espírito Santo, José; Ferreira, Gilda

We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell- Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of “administrative” redexes. These are the key, on the one hand, to understand the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said.

2019Journal article

Open access