+, ^+, and non-permutability of -steps
DOI10.1016/J.JSC.2011.12.035zbMATH Open1261.68108OpenAlexW1602540486MaRDI QIDQ429596FDOQ429596
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
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
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Untersuchungen über das logische Schliessen. I
- Isabelle/HOL. A proof assistant for higher-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Computational logic and proof theory. 3rd Kurt Gödel Colloquium, KGC '93, Brno, Czech Republic, August 24-27, 1993. Proceedings
- What you always wanted to know about rigid \(E\)-unification
- Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
- Mechanizing mathematical reasoning. Essays in honor of Jörg H. Siekmann on the occasion of his 60th birthday.
- The rise of modern logic: from Leibniz to Frege
- Automated deduction in classical and non-classical logics. Selected papers
- Shallow confluence of conditional term rewriting systems
- An even closer integration of linear arithmetic into inductive theorem proving
- Descente Infinie + Deduction
- Automated Reasoning with Analytic Tableaux and Related Methods
- Grundlagen der Mathematik I
- Mechanizing Mathematical Reasoning
- Mathematical Knowledge Management
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
- Hilbert's epsilon as an operator of indefinite committed choice
Uses Software
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)
