Algorithms, datastructures, and other issues in efficient automated deduction

DOI10.1007/3-540-45744-5_3MaRDI QIDQ4539595zbMATH OpenFDO

Authors Andrei Voronkov

Publication date 10 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2083/20830013

Mathematics Subject Classification ID

Recommendations

• Deduction as an engineering science
• Resolution theorem proving
• scientific article; zbMATH DE number 1360950
• scientific article; zbMATH DE number 13446
• scientific article; zbMATH DE number 1980923

Cited in

(8)

• A theory for deductive synthesis of algorithms in the computing milieu
• An efficient subsumption test pipeline for BS(LRA) clauses
• Alternating two-way AC-tree automata
• Resolution with order and selection for hybrid logics
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• Multi-completion with termination tools
• Deduction as an engineering science
• Citius altius fortius: lessons learned from the theorem prover Waldmeister

Describes a project that uses

Uses Software

• VAMPIRE
• SCOTT
• SystemOnTPTP
• SETHEO
• SPASS
• MBase
• Roo

This page was built for publication: Algorithms, datastructures, and other issues in efficient automated deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4539595)