scientific article; zbMATH DE number 6938205

MaRDI QIDQ5376325zbMATH OpenFDO

Authors Gela Chankvetadze, Lia Kurtanidze, Mikheil Rukhaia

Publication date 17 September 2018

zbMATH Keywords

formula schemataproof-searchsequent calculus

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
• A procedure for automatic proof nets construction
• scientific article; zbMATH DE number 863013
• A general method for using schematizations in automated deduction
• 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
• scientific article; zbMATH DE number 1389654
• Automatic construction of Hoare proofs from abstract interpretation results.

Cited in

(9)

• Proofs as schemas and their heuristic use
• Reasoning on schemas of formulas: an automata-based approach
• Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
• Higher-order proof construction based on first-order narrowing
• Automatic generation of proof search strategies for second-order logic
• Sequent schema for derived rules
• A general method for using schematizations in automated deduction
• Uniform schemata for proof rules
• scientific article; zbMATH DE number 3894495 (Why is no real title available?)

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)