\(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
DOI10.1016/j.jsc.2011.12.035zbMath1261.68108OpenAlexW1602540486MaRDI QIDQ429596
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
- Hilbert's epsilon as an operator of indefinite committed choice
- 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
- Isabelle/HOL. A proof assistant for higher-order logic
- Mechanizing mathematical reasoning. Essays in honor of Jörg H. Siekmann on the occasion of his 60th birthday.
- Untersuchungen über das logische Schliessen. I
- 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
- Descente Infinie + Deduction
- Automated Reasoning with Analytic Tableaux and Related Methods
- Grundlagen der Mathematik I
- Mechanizing Mathematical Reasoning
- Mathematical Knowledge Management
This page was built for publication: \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
