scientific article; zbMATH DE number 1543300
From MaRDI portal
Publication:4520767
zbMath0961.68116MaRDI QIDQ4520767
Publication date: 27 February 2001
Full work available at URL: http://www.jucs.org/jucs_5_3/a_generic_tableau_prover
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Semi-intelligible Isar proofs from machine-generated proofs, Automatic Proof and Disproof in Isabelle/HOL, Computational logic: its origins and applications, Verifying the SET purchase protocols, A proof-centric approach to mathematical assistants, Automation for interactive proof: first prototype, On theorem prover-based testing, The Isabelle Framework, On the mechanization of the proof of Hessenberg's theorem in coherent logic, Proving pointer programs in higher-order logic, From LCF to Isabelle/HOL, A general tableau method for propositional interval temporal logics: theory and implementation, Sort It Out with Monotonicity, Lightweight relevance filtering for machine-generated resolution problems, Effective Normalization Techniques for HOL, AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic, Mechanized metatheory revisited, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
