SPASS+T

Virgile Prevosto; Uwe Waldmann

SPASS+T

Virgile Prevosto
, Uwe Waldmann

LIST-DTSI-SLA CEA
Max-Planck-Institut fur Informatik

Résultats de recherche: Contribution à un journal › Article de conférence › Revue par des pairs

Résumé

Spass+T is an extension of the superposition-based theorem prover Spass that allows us to enlarge the reasoning capabilities of Spass using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of Spass+T and the capabilities, limitations, and applications of such a combination.

langue originale	Anglais
Pages (de - à)	18-33
Nombre de pages	16
journal	CEUR Workshop Proceedings
Volume	192
état	Publié - 1 déc. 2006
Modification externe	Oui
Evénement	FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, ESCoR 2006 - Seattle, WA, États-Unis Durée: 22 août 2006 → 22 août 2006

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

@article{28f2d9f298d7450d94d29e87cdd69113,

title = "SPASS+T",

abstract = "Spass+T is an extension of the superposition-based theorem prover Spass that allows us to enlarge the reasoning capabilities of Spass using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of Spass+T and the capabilities, limitations, and applications of such a combination.",

author = "Virgile Prevosto and Uwe Waldmann",

year = "2006",

month = dec,

day = "1",

language = "English",

volume = "192",

pages = "18--33",

journal = "CEUR Workshop Proceedings",

issn = "1613-0073",

note = "FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, ESCoR 2006 ; Conference date: 22-08-2006 Through 22-08-2006",

}

TY - JOUR

T1 - SPASS+T

AU - Prevosto, Virgile

AU - Waldmann, Uwe

PY - 2006/12/1

Y1 - 2006/12/1

N2 - Spass+T is an extension of the superposition-based theorem prover Spass that allows us to enlarge the reasoning capabilities of Spass using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of Spass+T and the capabilities, limitations, and applications of such a combination.

AB - Spass+T is an extension of the superposition-based theorem prover Spass that allows us to enlarge the reasoning capabilities of Spass using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of Spass+T and the capabilities, limitations, and applications of such a combination.

UR - https://www.scopus.com/pages/publications/79959729624

M3 - Conference article

AN - SCOPUS:79959729624

SN - 1613-0073

VL - 192

SP - 18

EP - 33

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

T2 - FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, ESCoR 2006

Y2 - 22 August 2006 through 22 August 2006

ER -

SPASS+T

Résumé

Autres fichiers et liens

Empreinte digitale

Contient cette citation