×

IsaFoL

swMATH ID: 19193
Software Authors: Blanchette, J.C., Fleury, M., Schlichtkrull, A., Traytel, D.
Description: IsaFoL: Isabelle Formalization of Logic. This repository contains various ongoing Isabelle formalizations of logical calculi. The goal is to develop lemma libraries and methodology for formalizing modern research in automated reasoning. Our initial focus is on well-established ground and first-order calculi, such as DPLL, CDCL, and resolution. One of our inspirations is the IsaFoR/CeTA project (Isabelle/HOL Formalization of Rewriting for Certified Termination Analysis) at Universität Innsbruck.
Homepage: https://bitbucket.org/isafol/isafol/wiki/Home
Dependencies: Isabelle
Related Software: Archive Formal Proofs; Isabelle/HOL; Completeness theorem; Sledgehammer; Isabelle; FOL Fitting; Isar; SPASS; SAT Solver Verification; AVATAR; Locales; versat; Chaff; z3; VAMPIRE; HOL; FOL_Harrison; Propositional Resolution; Incredible Proof Machine; Abstract Soundness
Referenced in: 4 Publications

Referenced in 1 Serial

2 Journal of Automated Reasoning

Referencing Publications by Year