scientific article; zbMATH DE number 6938205

MaRDI QIDQ5376325zbMATH OpenFDO

Authors Gela Chankvetadze, Lia Kurtanidze, Mikheil Rukhaia

Publication date 17 September 2018

zbMATH Keywords

sequent calculusproof-searchformula schemata

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Automated constructivization of proofs
• scientific article; zbMATH DE number 1324433
• scientific article; zbMATH DE number 863013
• scientific article; zbMATH DE number 1765701
• scientific article; zbMATH DE number 2100042
• Automatic Proof Generation in Kleene Algebra
• scientific article; zbMATH DE number 3894495
• A formal proof generator from semi-formal proof documents
• Publication:4934147
• Automatic construction of Hoare proofs from abstract interpretation results.

Cited in

(9)

• scientific article; zbMATH DE number 1927428 (Why is no real title available?)
• Reasoning on schemas of formulas: an automata-based approach
• scientific article; zbMATH DE number 3894495 (Why is no real title available?)
• scientific article; zbMATH DE number 1341622 (Why is no real title available?)
• Uniform schemata for proof rules
• scientific article; zbMATH DE number 1765701 (Why is no real title available?)
• Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
• Proofs as schemas and their heuristic use
• Higher-order proof construction based on first-order narrowing

This page was built for publication:

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