Extensional higher-order paramodulation in Leo-III (Q2666959): Difference between revisions

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