Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: theorem provers

Sortuj według:

Ogranicz wyniki do:

JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi

Ferrari M., Fiorentini C., Fiorino G.

Fundamenta Informaticae

2017

Vol. 150, nr 1

119--142

JTabWb is a Java framework for developing provers based on sequent or tableau calculi. It provides a generic engine which searches for proof of a given goal driven by a user-defined prover. The user is required to define the components of a prover by implementing suitable Java interfaces. In this paper we describe the structure of the framework and the role of its components through a running example. To show the generality of the framework we review some of the provers implemented in JTabWb. Finally, to corroborate the fact that the framework can be used to generate efficient provers, we compare the performances of one of the implemented provers with the state-of-the-art provers for Intuitionistic Propositional Logic.

Specification and integration of theorem provers and computer algebra systems

Bertoli P.G., Calmet J., Giunchiglia F., Homann K.

Fundamenta Informaticae

1999

Vol. 39, Nr 1,2

39-57

Computer algebra systems (CASs) and automated theorem provers (ATPs) exhibit complementary abilities. CASs focus on efficiently solving domain-specific problems. ATPs are designed to allow for the formalization and solution of wide classes of problems within some logical framework. Integrating CASs and ATPs allows for the solution of problems of a higher complexity than those confronted by each class alone. However, most experiments conducted so far followed an ad-hoc approach, resulting in solutions tailored to specific problems. A structured and principled approach is necessary to allow for the sound integration of systems in a modular way. The Open Mechanized Reasoning Systems (OMRS) framework was introduced for the specification and implementation of mechanized reasoning systems, e.g. ATPs. In this paper, we introduce a generalization of OMRS, named OMSCS (Open Mechanized Symbolic Computation Systems). We show how OMSCS can be used to soundly express CASs, ATPs, and their integration, by formalizing a combination between the Isabelle prover and the Maple algebra system. We show how the integrated system solves a problem which could not be tackled by each single system alone.