|
|
(24 intermediate revisions by 4 users not shown) |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOL Light / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: QMLTP / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Leo / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: DISCOUNT / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Coq / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Isabelle/HOL / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOL / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Sledgehammer / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: CVC4 / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Nitpick / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: VAMPIRE / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: iProver / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: E Theorem Prover / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Easychair / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: LeoPARD / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: MSPASS / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Leo-III / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: FMLtoHOL / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: MleanCoP / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: embed_modal / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Satallax / rank |
| | Normal rank |
| Property / MaRDI profile type |
| | |
| Property / MaRDI profile type: MaRDI publication profile / rank |
| | Normal rank |
| Property / OpenAlex ID |
| | |
| Property / OpenAlex ID: W3148132267 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Explicit substitutions / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Resolution in type theory / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: General models and extensionality / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: General models, descriptions, and choice in type theory / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: An introduction to mathematical logic and type theory: To truth through proof. / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q2723416 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: TPS: A hybrid automatic-interactive system for developing proofs / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3343471 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Extending SMT solvers to higher-order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Functional calculus of first order based on strict implication / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3077958 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Superposition with lambdas / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Superposition for \(\lambda\)-free higher-order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4263170 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Combining and automating classical and non-classical logics in classical higher-order logics / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Cut-elimination for quantified conditional logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Higher-order semantics and extensionality / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Cut-Simulation and Impredicativity / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5224901 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4619819 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3457212 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Multimodal and intuitionistic logics in simple type theory / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Quantified multimodal logics in simple type theory / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: HOL Based First-Order Modal Logic Provers / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Automating Free Logic in Isabelle/HOL / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The higher-order prover \textsc{Leo}-II / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Computer-assisted analysis of the Anderson-Hájek ontological controversy / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Restricted combinatory unification / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3408862 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Extending Sledgehammer with SMT solvers / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Encoding Monomorphic and Polymorphic Types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Satallax: An Automatic Higher-Order Prover / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: GRUNGE: a grand unified ATP challenge / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5667469 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Linear Spine Calculus / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Handling Polymorphism in Automated Deduction / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The MET: The Art of Flexible Reasoning with Modalities / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Theorem Provers For Every Normal Modal Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The undecidability of the second-order unification problem / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5287513 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: HOL Light: An Overview / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Completeness in the theory of types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The undecidability of unification in third order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q2721185 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Alpha-conversion and typability / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Focused Sequent Calculus for Higher-Order Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Translating higher-order clauses to first-order clauses / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Lightweight relevance filtering for machine-generated resolution problems / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Intensional models for the theory of types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4264721 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: MleanCoP: A Connection Prover for First-Order Modal Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The QMLTP Problem Library for First-Order Modal Logics / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3150300 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5624683 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3150301 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Computer supported mathematics with \(\Omega\)MEGA / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Brief Overview of HOL4 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Higher-order unification revisited: Complete sets of transformations / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4557854 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The higher-order prover Leo-III / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Agent-Based HOL Reasoning / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3075241 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The TPTP Typed First-Order Form with Arithmetic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Effective Normalization Techniques for HOL / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: On restrictions of ordered paramodulation with simplification / rank |
| | Normal rank |