scientific article; zbMATH DE number 1543300
From MaRDI portal
Publication:4520767
zbMATH Open0961.68116MaRDI QIDQ4520767FDOQ4520767
Authors: Lawrence C. Paulson 
Publication date: 27 February 2001
Full work available at URL: http://www.jucs.org/jucs_5_3/a_generic_tableau_prover
Title of this publication is not available (Why is that?)
Recommendations
Cited In (24)
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- A framework for using knowledge in tableau proofs
- A general tableau method for propositional interval temporal logics: theory and implementation
- Mechanized metatheory revisited
- The Isabelle Framework
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- Semi-intelligible Isar proofs from machine-generated proofs
- Verifying the SET purchase protocols
- A proof-centric approach to mathematical assistants
- Title not available (Why is that?)
- Effective normalization techniques for HOL
- Lightweight relevance filtering for machine-generated resolution problems
- On theorem prover-based testing
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- From LCF to Isabelle/HOL
- Computational logic: its origins and applications
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Proving pointer programs in higher-order logic
- Automating automated reasoning. The case of two generic automated reasoning tools
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Automatic proof and disproof in Isabelle/HOL
- Automation for interactive proof: first prototype
- AUTO2, a saturation-based heuristic prover for higher-order logic
Uses Software
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 Q4520767)
