본문 바로가기
HOME> 저널/프로시딩 > 저널/프로시딩 검색상세

저널/프로시딩 상세정보

권호별목차 / 소장처보기

H : 소장처정보

T : 목차정보

Journal of symbolic computation 8건

  1. [해외논문]   Editorial Board  


    Journal of symbolic computation v.90 ,pp. ii - ii , 2019 , 0747-7171 ,

    초록

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  2. [해외논문]   Symbolic computation in software science  

    Davenport, James Harold
    Journal of symbolic computation v.90 ,pp. 1 - 2 , 2019 , 0747-7171 ,

    초록

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  3. [해외논문]   Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques  

    Dră (West University of Timişoara, Romania ) , mnesc, Isabela (RISC, Johannes Kepler University, Linz, Austria ) , Jebelean, Tudor (Université) , Stratulat, Sorin (de Lorraine, CNRS, LORIA, F-57000 Metz, France)
    Journal of symbolic computation v.90 ,pp. 3 - 41 , 2019 , 0747-7171 ,

    초록

    Abstract We develop logic and combinatorial methods for automating the generation of sorting algorithms for binary trees, starting from input-output specifications and producing conditional rewrite rules. The main approach consists in proving (constructively) the existence of an appropriate output from every input. The proof may fail if some necessary sub-algorithms are lacking. Then, their specifications are suggested and their synthesis is performed by the same principles. Our main goal is to avoid the possibly prohibitive cost of pure resolution proofs by using a natural-style proving in which domain-specific strategies and inference steps lead to a significant increase of efficiency. In addition to classical techniques for natural-style proving, we introduce novel ones (priority of certain types of assumptions, transformation of elementary goals into conditions, special criteria for decomposition of the goal and of the assumptions), as well as methods based on the properties of domain-specific relations and functions. In particular, we use combinatorial techniques in order to generate possible witnesses, which in certain cases lead to the discovery of new induction principles. From the proof, the algorithm is extracted by transforming inductive proof steps into recursions, and case-based proof steps into conditionals. The approach is demonstrated in parallel using the Theorema system, by developing the theory, implementing the prover, and performing the proofs of the necessary properties and synthesis conjectures. It is also validated in the Coq system, which allows to compare the facilities of the two systems from the point of view of our application.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  4. [해외논문]   Nominal unification with atom-variables  

    Schmidt-Schauß, Manfred , Sabel, David , Kutz, Yunus D.K.
    Journal of symbolic computation v.90 ,pp. 42 - 64 , 2019 , 0747-7171 ,

    초록

    Abstract The problem of nominal unification where variables are allowed for atoms, and computing a complete set of unifiers is considered. The complexity is shown to be NP-complete, while for special cases there are polynomial time algorithms. The main result is a novel algorithm to compute a complete set of unifiers which performs lazy guessing of equality or disequality of atom-variables, runs in NP time, and the collecting variant has more chances to keep the complete set of unifiers small. Applications of this algorithm are in reasoning about program transformations in higher order functional languages. We also present a variant of the unification algorithm that delays guessing and checking solvability, and produces a single most general unifier.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  5. [해외논문]   Formal analysis of continuous-time systems using Fourier transform  

    Rashid, Adnan , Hasan, Osman
    Journal of symbolic computation v.90 ,pp. 65 - 88 , 2019 , 0747-7171 ,

    초록

    Abstract To study the dynamical behavior of the engineering and physical systems, we often need to capture their continuous behavior, which is modeled using differential equations, and perform the frequency-domain analysis of these systems. Traditionally, Fourier transform methods are used to perform this frequency domain analysis using paper-and-pencil based analytical techniques or computer simulations. However, both of these methods are error prone and thus are not suitable for analyzing systems used in safety-critical domains, like medicine and transportation. In order to provide an accurate alternative, we propose to use higher-order-logic theorem proving to conduct the frequency domain analysis of these systems. For this purpose, the paper presents a higher-order-logic formalization of Fourier transform using the HOL-Light theorem prover. In particular, we use the higher-order-logic based formalizations of differential, integral, transcendental and topological theories of multivariable calculus to formally define Fourier transform and reason about the correctness of its classical properties, such as existence, linearity, time shifting, frequency shifting, modulation, time scaling, time reversal and differentiation in time domain, and its relationships with Fourier Cosine, Fourier Sine and Laplace transforms. We use our proposed formalization for the formal verification of the frequency response of a generic n-order linear system, an audio equalizer and a MEMs accelerometer, using the HOL-Light theorem prover.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  6. [해외논문]   Aligning concepts across proof assistant libraries  

    Gauthier, Thibault , Kaliszyk, Cezary
    Journal of symbolic computation v.90 ,pp. 89 - 123 , 2019 , 0747-7171 ,

    초록

    Abstract As the knowledge available in the computer understandable proof corpora grows, recognizing repeating patterns becomes a necessary requirement in order to organize, synthesize, share, and transmit ideas. In this work, we automatically discover patterns in the libraries of interactive theorem provers and thus provide the basis for such applications for proof assistants. This involves detecting close properties, inducing the presence of matching concepts, as well as dynamically evaluating the quality of matches from the similarity of the environment of each concept. We further propose a classification process, which involves a disambiguation mechanism to decide which concepts actually represent the same mathematical ideas. We evaluate the approach on the libraries of six proof assistants based on different logical foundations: HOL4, HOL Light, and Isabelle/HOL for higher-order logic, Coq and Matita for intuitionistic type theory, and the Mizar Mathematical Library for set theory. Comparing the structures available in these libraries our algorithm automatically discovers hundreds of isomorphic concepts and thousands of highly similar ones.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  7. [해외논문]   Using jointly geometry and algebra to determine RC-constructibility  

    Schreck, Pascal , Mathis, Pascal
    Journal of symbolic computation v.90 ,pp. 124 - 148 , 2019 , 0747-7171 ,

    초록

    Abstract In most cases in geometry, applying analytic or algebraic tools on coordinates helps to solve some difficult problems. For instance, proving that a geometrical construction problem is solvable using ruler and compass is often impossible within a synthetic geometry framework. But in an analytic geometry framework, it is a direct application of Galois theory after performing triangularizations. However, these algebraic tools lead to a large amount of computation. Their implementation in modern Computer Algebra Systems (CAS) are still too time consuming to provide an answer in a reasonable time. In addition, they require a lot of memory space which can grow exponentially with the size of the problem. Fortunately, some geometrical properties can be used to setup the algebraic systems so that they can be more efficiently computed. These properties turn polynomials into new ones so as to reduce both the degrees and the number of monomials. The present paper promotes this approach by considering two corpora of geometric construction problems, namely Wernick's and Connely's lists. These lists contain about 280 problems. The purpose is to determine their status i.e. whether they are constructible or not with ruler and compass. Some of these problems had unknown status that will be settled in this paper. More generally, the status of all problems of these corpora are fully automatically given by an approach combining geometry and algebra.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  8. [해외논문]   Formalization of the arithmetization of Euclidean plane geometry and applications  

    Boutry, Pierre , Braun, Gabriel , Narboux, Julien
    Journal of symbolic computation v.90 ,pp. 149 - 168 , 2019 , 0747-7171 ,

    초록

    Abstract This paper describes the formalization of the arithmetization of Euclidean plane geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamathematical properties. This work completes our formalization of the two-dimensional results contained in part one of the book by SchwabhAuser, Szmielew and Tarski Metamathematische Methoden in der Geometrie . We defined the arithmetic operations geometrically and proved that they verify the properties of an ordered field. Then, we introduced Cartesian coordinates, and provided characterizations of the main geometric predicates. In order to prove the characterization of the segment congruence relation, we provided a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras' theorems. To obtain the characterizations of the geometric predicates, we adopted an original approach based on bootstrapping: we used an algebraic prover to obtain new characterizations of the predicates based on already proven ones. The arithmetization of geometry paves the way for the use of algebraic automated deduction methods in synthetic geometry. Indeed, without a “back-translation” from algebra to geometry, algebraic methods only prove theorems about polynomials and not geometric statements. However, thanks to the arithmetization of geometry, the proven statements correspond to theorems of any model of Tarski's Euclidean geometry axioms. To illustrate the concrete use of this formalization, we derived from Tarski's system of geometry a formal proof of the nine-point circle theorem using the GrObner basis method. Moreover, we solve a challenge proposed by Beeson: we prove that, given two points, an equilateral triangle based on these two points can be constructed in Euclidean Hilbert planes. Finally, we derive the axioms for another automated deduction method: the area method.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지

논문관련 이미지