SAD as a mathematical assistant -- how should we go from here to there?

DOI10.1016/j.jal.2005.10.009zbMath1107.68099OpenAlexW2015546518MaRDI QIDQ865654

Alexander Lyaletski, Konstantin Verchinine, Andrei Paskevich

Publication date: 20 February 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.009

zbMATH Keywords

automated reasoningproof assistantformalizing mathematics

Mathematics Subject Classification ID

Related Items

Glushkov's evidence algorithm, SAD, On Correctness of Mathematical Texts from a Logical and Practical Point of View

Uses Software

• Coq
• Theorema
• ML
• Isabelle/HOL
• IsaPlanner
• OTTER
• VAMPIRE
• PVS
• Haskell
• SPASS
• TPTP
• Isar
• Mizar
• HOL
• Automath
• NQTHM
• ForTheL
• Lambda-Clam

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• Untersuchungen über das logische Schliessen. I
• A refinement of de Bruijn's formal language of mathematics
• Proving Theorems with the Modification Method
• Goal directed strategies for paramodulation
• The TPTP problem library
• Ωmega: Towards a mathematical assistant
• Mathematical Knowledge Management
• Some problems in the theories of automata and artificial intelligence