On the public citation graph

Extensional Higher-Order Paramodulation and RUE-Resolution

https://doi.org/10.1007/3-540-48660-7_39
0 signed · 42 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/978-3-642-81955-1_29openalex-snapshot
Resolution in Type Theory
inferredcites →https://doi.org/10.1007/978-94-015-9934-4openalex-snapshot
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
inferredcites →https://doi.org/10.1007/bfb0054239openalex-snapshot
Automated Deduction — CADE-15
inferredcites →https://doi.org/10.1007/bfb0054248openalex-snapshot
Extensional higher-order resolution
inferredcites →https://doi.org/10.1007/bfb0054256openalex-snapshot
System description: Leo — A higher-order theorem prover
inferredcites →https://doi.org/10.1016/c2009-0-14341-6openalex-snapshot
The Lambda Calculus - Its Syntax and Semantics
inferredcites →https://doi.org/10.1016/s0747-7171(89)80023-9openalex-snapshot
Higher-order unification revisited: Complete sets of transformations
inferredcites →https://doi.org/10.1017/cbo9780511569906openalex-snapshot
The Clausal Theory of Types
inferredcites →https://doi.org/10.1073/pnas.49.6.828openalex-snapshot
A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
inferredcites →https://doi.org/10.22028/d291-25680openalex-snapshot
Equality and extensionality in automated higher-order theorem proving
inferredcites →https://doi.org/10.22028/d291-25891openalex-snapshot
A mechanization of sorted higher-order logic based on the resolution principle
inferredcites →https://doi.org/10.22028/d291-41622openalex-snapshot
Model Existence for Higher Order Logic
inferredcites →https://doi.org/10.2307/2266170openalex-snapshot
A formulation of the simple theory of types
inferredcites →https://doi.org/10.2307/2266967openalex-snapshot
Completeness in the theory of types
inferredcites →https://doi.org/10.2307/2269949openalex-snapshot
Resolution in type theory
inferredcites →https://doi.org/10.2307/2274454openalex-snapshot
Peter B. Andrews. An introduction to mathematical logic and type theory: to truth through proof. Computer science and applied mathematics. Academic Press, Orlando etc. 1986, xv + 304 pp.

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.2139/ssrn.3198954openalex-extracted
inferred← citeshttps://doi.org/10.1007/978-3-030-29436-6_4openalex-snapshot
Superposition with Lambdas
inferred← citeshttps://doi.org/10.1007/978-3-030-79876-5_22openalex-snapshot
Superposition with First-class Booleans and Inprocessing Clausification
inferred← citeshttps://doi.org/10.1007/978-3-540-32275-7_27openalex-snapshot
Can a Higher-Order and a First-Order Theorem Prover Cooperate?
inferred← citeshttps://doi.org/10.1007/978-3-642-02716-1_11openalex-snapshot
Terminating Tableaux for the Basic Fragment of Simple Type Theory
inferred← citeshttps://doi.org/10.1007/s10472-011-9249-7openalex-snapshot
Combining and automating classical and non-classical logics in classical higher-order logics
inferred← citeshttps://doi.org/10.1007/s10817-015-9348-yopenalex-snapshot
The Higher-Order Prover Leo-II
inferred← citeshttps://doi.org/10.1007/s10817-021-09588-xopenalex-snapshot
Extensional Higher-Order Paramodulation in Leo-III
inferred← citeshttps://doi.org/10.1007/s10817-021-09595-yopenalex-snapshot
Superposition with Lambdas
inferred← citeshttps://doi.org/10.1007/s10992-016-9403-0openalex-snapshot
Cut-Elimination for Quantified Conditional Logic
inferred← citeshttps://doi.org/10.1007/s13218-019-00628-8openalex-snapshot
Extensional Paramodulation for Higher-Order Logic and Its Effective Implementation Leo-III
inferred← citeshttps://doi.org/10.1016/b978-0-444-51624-4.50005-8openalex-snapshot
Automation of Higher-Order Logic
inferred← citeshttps://doi.org/10.1016/b978-044450813-3/50017-5openalex-snapshot
Classical Type Theory
inferred← citeshttps://doi.org/10.1016/j.websem.2011.11.008openalex-snapshot
Higher-order aspects and context in SUMO
inferred← citeshttps://doi.org/10.1023/a:1020840027781openalex-snapshot
Comparing Approaches To Resolution Based Higher-Order Theorem Proving
inferred← citeshttps://doi.org/10.1609/aimag.v37i2.2620openalex-snapshot
The CADE ATP System Competition — CASC
inferred← citeshttps://doi.org/10.2168/lmcs-6(2:3)2010openalex-snapshot
Analytic Tableaux for Simple Type Theory and its First-Order Fragment
inferred← citeshttps://doi.org/10.2178/jsl/1102022211openalex-snapshot
Higher-order semantics and extensionality
inferred← citeshttps://doi.org/10.29007/grmxopenalex-snapshot
Leo-III Version 1.1 (System description)
inferred← citeshttps://doi.org/10.29007/jgkwopenalex-snapshot
Going Polymorphic - TH1 Reasoning for Leo-III
inferred← citeshttps://doi.org/10.29007/lbxwopenalex-snapshot
LEO-II Version 1.5
inferred← citeshttps://doi.org/10.29007/lvccopenalex-snapshot
Proceedings of the 6th IJCAR ATP System Competition (CASC-J6)
inferred← citeshttps://doi.org/10.29007/x9c9openalex-snapshot
Understanding LEO-II’s proofs
inferred← citeshttps://doi.org/10.48550/arxiv.2102.00453openalex-snapshot
Superposition with Lambdas
inferred← citeshttps://doi.org/10.5220/0004324803460351openalex-snapshot
A Top-down Approach to Combining Logics
inferred← citeshttps://doi.org/10.6092/issn.1972-5787/1710openalex-snapshot
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.