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

From MaRDI portal
Changed an Item
ReferenceBot (talk | contribs)
Changed an Item
 
(22 intermediate revisions by 4 users not shown)
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

Latest revision as of 12:02, 4 December 2024

scientific article
Language Label Description Also known as
English
Extensional higher-order paramodulation in Leo-III
scientific article

    Statements

    Extensional higher-order paramodulation in Leo-III (English)
    0 references
    0 references
    0 references
    23 November 2021
    0 references
    higher-order logic
    0 references
    Henkin semantics
    0 references
    extensionality
    0 references
    Leo-III
    0 references
    equational reasoning
    0 references
    automated theorem proving
    0 references
    nonclassical logics
    0 references
    quantified modal logics
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references