+, ^+, and non-permutability of -steps

DOI10.1016/J.JSC.2011.12.035MaRDI QIDQ429596zbMATHOpenAlexFDO

Authors Claus-Peter Wirth

Publication date 20 June 2012

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2011.12.035

zbMATH Keywords

automated theorem proving\(\delta ^{+}\)-ruleformal proofs of standard theoremsfree-variable calculihuman-oriented computer-assisted proof constructionliberalized \(\delta \)-rulesmathematics assistance systemsnon-permutability of reductive inference rulesreductive calculi

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Permutability of proofs in intuitionistic sequent calculi
• scientific article; zbMATH DE number 1507185
• Issues in the analysis of proof-search strategies in sequential presentations of logics
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• scientific article; zbMATH DE number 1552525

Cites work

• scientific article; zbMATH DE number 47007 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 1341475 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 1507185 (Why is no real title available?)
• scientific article; zbMATH DE number 2090295 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3207266 (Why is no real title available?)
• scientific article; zbMATH DE number 3237808 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• An even closer integration of linear arithmetic into inductive theorem proving
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
• Automated deduction in classical and non-classical logics. Selected papers
• Computational logic and proof theory. 3rd Kurt Gödel Colloquium, KGC '93, Brno, Czech Republic, August 24-27, 1993. Proceedings
• Descente Infinie + Deduction
• Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous
• Grundlagen der Mathematik I
• Hilbert's epsilon as an operator of indefinite committed choice
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematical Knowledge Management
• Mechanizing Mathematical Reasoning
• Mechanizing mathematical reasoning. Essays in honor of Jörg H. Siekmann on the occasion of his 60th birthday.
• Shallow confluence of conditional term rewriting systems
• The rise of modern logic: from Leibniz to Frege
• Untersuchungen über das logische Schliessen. I
• What you always wanted to know about rigid \(E\)-unification

Describes a project that uses

Uses Software

• Coq
• QuodLibet

This page was built for publication: \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps

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