SAD as a mathematical assistant -- how should we go from here to there?
type: Item
instance of: scholarly article
title: SAD as a mathematical assistant -- how should we go from here to there?
zbMATH Open document ID: 1107.68099
author: Alexander Lyaletski
author: Konstantin Verchinine
author: Andrei Paskevich
published in: Journal of Applied Logic
publication date: 2007-02-20T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5128351
zbMATH Keywords: formalizing mathematics
zbMATH Keywords: automated reasoning
zbMATH Keywords: proof assistant
describes a project that uses: Coq
describes a project that uses: IsaPlanner
describes a project that uses: PVS
describes a project that uses: Automath
describes a project that uses: ForTheL
describes a project that uses: Mizar
describes a project that uses: ML
describes a project that uses: Haskell
describes a project that uses: SPASS
describes a project that uses: TPTP
describes a project that uses: Isar
describes a project that uses: Lambda-Clam
describes a project that uses: VAMPIRE
describes a project that uses: OTTER
describes a project that uses: Theorema
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL
describes a project that uses: NQTHM
MaRDI profile type: Publication
full work available at URL: j.jal.2005.10.009
OpenAlex ID: W2015546518
cites work: Some problems in the theories of automata and artificial intelligence
cites work: Mathematical Knowledge Management
cites work: Model elimination and connection tableau procedures
cites work: Proving Theorems with the Modification Method
cites work: Q4809064
cites work: Q3150300
cites work: The TPTP problem library
cites work: Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: A refinement of de Bruijn's formal language of mathematics
cites work: Combinatory logic. With two sections by William Craig.
cites work: Q5573961
cites work: Q4471536
cites work: Untersuchungen über das logische Schliessen. I
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Ωmega: Towards a mathematical assistant
cites work: Q5287513
cites work: Q4040283
cites work: Q4226993
cites work: Goal directed strategies for paramodulation
DOI: 10.1016/J.JAL.2005.10.009
description: scientific article; zbMATH DE number 5128351