Search results for "paramodulation"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
116	Andrey Paskevich	Connection Tableaux with Lazy Paramodulation.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Connection tableaux, Lazy paramodulation, Basic ordered paramodulation, First-order logic with equality
106	Christopher Lynch, Duc-Khanh Tran	Automatic Decidability and Combinability Revisited.	CADE	2007	DBLP DOI BibTeX RDF
100	Wayne Snyder, Christopher Lynch	Goal Directed Strategies for Paramodulation.	RTA	1991	DBLP DOI BibTeX RDF
100	Dan Benanav	Simultaneous Paramodulation.	CADE	1990	DBLP DOI BibTeX RDF
91	Richard B. Scherl	Equality and Constrained Resolution.	JELIA	1994	DBLP DOI BibTeX RDF
85	Larry Wos, Ross A. Overbeek, Lawrence J. Henschen	Hyperparamodulation: A Refinement of Paramodulation.	CADE	1980	DBLP DOI BibTeX RDF
70	Paul Y. Gloess, Jean-Pierre H. Laurent	Adding Dynamic Paramodulation to Rewrite Algorithms.	CADE	1980	DBLP DOI BibTeX RDF	critical pairs, Knuth-Bendix algorithm, paramodulation, rewrite algorithms, theorem-proving, rewrite rules
70	Miquel Bofill, Albert Rubio	Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation.	CADE	2002	DBLP DOI BibTeX RDF
70	Miquel Bofill, Guillem Godoy	On the Completeness of Arbitrary Selection Strategies for Paramodulation.	ICALP	2001	DBLP DOI BibTeX RDF	automated deduction
70	Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder	Basic Paramodulation and Superposition.	CADE	1992	DBLP DOI BibTeX RDF
70	Larry Wos, William McCune	Negative Paramodulation.	CADE	1986	DBLP DOI BibTeX RDF
55	Andrey Paskevich	Connection Tableaux with Lazy Paramodulation.	IJCAR	2006	DBLP DOI BibTeX RDF
55	Miquel Bofill, Albert Rubio	Redundancy Notions for Paramodulation with Non-monotonic Orderings.	IJCAR	2004	DBLP DOI BibTeX RDF
55	Christoph Benzmüller	Extensional Higher-Order Paramodulation and RUE-Resolution.	CADE	1999	DBLP DOI BibTeX RDF
46	Rolf Socher-Ambrosius	A Refined Version of General E-Unification.	CADE	1994	DBLP DOI BibTeX RDF
40	Qing Liu 0011	lambda-Level Rough Equality Relation and the Inference of Rough Paramodulation.	Rough Sets and Current Trends in Computing	2000	DBLP DOI BibTeX RDF
40	Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio	Paramodulation with Non-Monotonic Orderings.	LICS	1999	DBLP DOI BibTeX RDF	term rewriting, automated deduction
40	Christian G. Fermüller, Gernot Salzer	Ordered Paramodulation and Resolution as Decision Procedure.	LPAR	1993	DBLP DOI BibTeX RDF
40	Nicolas Zabel	An Ordered Resolution and Paramodulation Calculus for Finite Many-Valued Logics.	JELIA	1992	DBLP DOI BibTeX RDF
40	Leo Bachmair, Harald Ganzinger	On Restrictions of Ordered Paramodulation with Simplification.	CADE	1990	DBLP DOI BibTeX RDF
40	Peter Padawitz	Inductive Proofs by Resolution and Paramodulation.	TAPSOFT, Vol.1	1989	DBLP DOI BibTeX RDF
40	Leo Bachmair	Proof Normalization for Resolution and Paramodulation.	RTA	1989	DBLP DOI BibTeX RDF
30	Peter Baumgartner 0001, Cesare Tinelli	The Model Evolution Calculus with Equality.	CADE	2005	DBLP DOI BibTeX RDF
30	Zohar Manna, Richard J. Waldinger	The Special-Relation Rules are Incomplete.	CADE	1992	DBLP DOI BibTeX RDF
30	Yusuf Ozturk, Lawrence J. Henschen	Hyper Resolution and Equality Axioms without Function Substitutions.	CADE	1990	DBLP DOI BibTeX RDF
30	Jia-Huai You, P. A. Subrahmanyam	On the Completeness of Narrowing for E-Unification.	KBCS	1989	DBLP DOI BibTeX RDF
30	Younghwan Lim	The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution.	CADE	1986	DBLP DOI BibTeX RDF
30	Jieh Hsiang, Michaël Rusinowitch	A New Method for Establishing Refutational Completeness in Theorem Proving.	CADE	1986	DBLP DOI BibTeX RDF
25	Ruo Ando, Yoshiyasu Takefuji	An experiment of the complexity of sliding block puzzles by 2D heat flow in paramodulation.	CoRR	2022	DBLP BibTeX RDF
25	Maria Paola Bonacina	Set of Support, Demodulation, Paramodulation: A Historical Perspective.	J. Autom. Reason.	2022	DBLP DOI BibTeX RDF
25	Grzegorz Prusak, Cezary Kaliszyk	Lazy Paramodulation in Practice.	PAAR@IJCAR	2022	DBLP BibTeX RDF
25	Xingxing He, Yang Xu 0001, Jun Liu 0001, Yingfang Li	α-Paramodulation method for a lattice-valued logic LnF(X) with equality.	Soft Comput.	2021	DBLP DOI BibTeX RDF
25	Alexander Steen, Christoph Benzmüller	Extensional Higher-Order Paramodulation in Leo-III.	J. Autom. Reason.	2021	DBLP DOI BibTeX RDF
25	Michael Rawson 0001, Giles Reger	lazyCoP: Lazy Paramodulation Meets Neurally Guided Search.	TABLEAUX	2021	DBLP DOI BibTeX RDF
25	Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen	Non-disjoint Combined Unification and Closure by Equational Paramodulation.	FroCoS	2021	DBLP DOI BibTeX RDF
25	Alexander Steen	Extensional Paramodulation for Higher-Order Logic and Its Effective Implementation Leo-III.	Künstliche Intell.	2020	DBLP DOI BibTeX RDF
25	Ruo Ando, Yoshiyasu Takefuji	A new perspective of paramodulation complexity by solving massive 8 puzzles.	CoRR	2020	DBLP BibTeX RDF
25	Alexander Steen, Christoph Benzmüller	Extensional Higher-Order Paramodulation in Leo-III.	CoRR	2019	DBLP BibTeX RDF
25	Alexander Steen	Extensional paramodulation for higher-order logic and its effective implementation Leo-III.		2018	RDF
25	Nicolas Peltier	A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules.	J. Log. Comput.	2017	DBLP DOI BibTeX RDF
25	Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv	Conjunctive Abstract Interpretation Using Paramodulation.	VMCAI	2017	DBLP DOI BibTeX RDF
25	Xingxing He, Yang Xu 0001, Jun Liu 0001	Alpha-Lock Paramodulation for Lattice-Valued Propositional Logic.	ISKE	2015	DBLP DOI BibTeX RDF
25	Michael Färber 0002, Cezary Kaliszyk	Metis-based Paramodulation Tactic for HOL Light.	GCAI	2015	DBLP DOI BibTeX RDF
25	Miquel Bofill, Albert Rubio	Paramodulation with Non-Monotonic Orderings and Simplification.	J. Autom. Reason.	2013	DBLP DOI BibTeX RDF
25	Gordon Stewart 0001, Lennart Beringer, Andrew W. Appel	Verified heap theorem prover by paramodulation.	ICFP	2012	DBLP DOI BibTeX RDF
25	Stephan Schulz 0001	Fingerprint Indexing for Paramodulation and Rewriting.	IJCAR	2012	DBLP DOI BibTeX RDF
25	Miquel Bofill, Albert Rubio	Paramodulation with Well-founded Orderings.	J. Log. Comput.	2009	DBLP DOI BibTeX RDF
25	Andrea Asperti, Enrico Tassi	Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
25	Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio	Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF
25	Robert Nieuwenhuis, Albert Rubio	Paramodulation-Based Theorem Proving.	Handbook of Automated Reasoning	2001	DBLP DOI BibTeX RDF
25	Guillem Godoy, Robert Nieuwenhuis	Paramodulation with Built-in Abelian Groups.	LICS	2000	DBLP DOI BibTeX RDF	term rewriting, automated deduction
25	Robert Nieuwenhuis	Decidability and Complexity Analysis by Basic Paramodulation.	Inf. Comput.	1998	DBLP DOI BibTeX RDF
25	Robert Nieuwenhuis, Albert Rubio	Paramodulation with Built-in AC-Theories and Symbolic Constraints.	J. Symb. Comput.	1997	DBLP DOI BibTeX RDF
25	Leo Bachmair	Paramodulation, Superposition, and Simplification.	Kurt Gödel Colloquium	1997	DBLP DOI BibTeX RDF
25	Robert Nieuwenhuis	Basic Paramodulation and Decidable Theories (Extended Abstract).	LICS	1996	DBLP DOI BibTeX RDF
25	Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder	Basic Paramodulation	Inf. Comput.	1995	DBLP DOI BibTeX RDF
25	Christopher Lynch	Paramodulation without Duplication	LICS	1995	DBLP DOI BibTeX RDF
25	Ralph Butler, Ross A. Overbeek	Formula Databases for High-Performance Resolution/Paramodulation Systems.	J. Autom. Reason.	1994	DBLP DOI BibTeX RDF
25	Gérard Becher, Uwe Petermann	Rigid Unification by Completion and Rigid Paramodulation.	KI	1994	DBLP DOI BibTeX RDF
25	Joachim Biskup	Relationship chase procedures interpreted as resolution with paramodulation.	Fundam. Informaticae	1991	DBLP BibTeX RDF
25	John Pais, Gerald E. Peterson	Using Forcing to Prove Completeness of Resolution and Paramodulation.	J. Symb. Comput.	1991	DBLP DOI BibTeX RDF
25	Hubert Bertling	Knuth-Bendix Completion of Horn Clause Programs for Restricted Linear Resolution and Paramodulation.	CTRS	1990	DBLP DOI BibTeX RDF
25	Hubert Bertling	Knuth-Bendix completion of Horn clause programs for restricted linear resolution and paramodulation.		1990	RDF
25	Ulrich Furbach, Steffen Hölldobler, Joachim F. Schreiber	Linear paramodulation modulo equality	Forschungsberichte, TU Munich	1989	RDF
25	Ulrich Furbach, Steffen Hölldobler, Joachim F. Schreiber	Horn Equational Theories and Paramodulation.	J. Autom. Reason.	1989	DBLP DOI BibTeX RDF
25	Ulrich Furbach, Steffen Hölldobler, Joachim F. Schreiber	Linear Paramodulation modulo Equality.	GWAI	1989	DBLP DOI BibTeX RDF
25	Xuhua Liu	Lock, Linear Lambda-Paramodulation in Operator Fuzzy Logic.	IJCAI	1989	DBLP BibTeX RDF
25	Yoshiyasu Takefuji, Michael Dowell	Novel approach to a rule-based general purpose program translator using paramodulation.	Knowl. Based Syst.	1988	DBLP DOI BibTeX RDF
25	Larry Wos	The Problem of Finding a Strategy to Control Binary Paramodulation.	J. Autom. Reason.	1988	DBLP DOI BibTeX RDF
25	Larry Wos	The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation.	J. Autom. Reason.	1988	DBLP DOI BibTeX RDF
25	Steffen Hölldobler	From Paramodulation to Narrowing.	ICLP/SLP	1988	DBLP BibTeX RDF
25	Christoph Walther	A Many-Sorted Calculus Based on Resolution and Paramodulation.		1987	RDF
25	Ulrich Furbach	Oldy but Goody Paramodulation Revisited.	GWAI	1987	DBLP DOI BibTeX RDF
25	Dieter Hutter	Using Resolution and Paramodulation for Induction Proofs.	GWAI	1986	DBLP DOI BibTeX RDF
25	William McCune, Lawrence J. Henschen	Experiments with Semantic Paramodulation.	J. Autom. Reason.	1985	DBLP DOI BibTeX RDF
25	Manfred Schmidt-Schauß	A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation.	IJCAI	1985	DBLP BibTeX RDF
25	Christoph Walther	A Many-Sorted Calculus Based on Resolution and Paramodulation.	IJCAI	1983	DBLP BibTeX RDF
25	William McCune, Lawrence J. Henschen	Semantic Paramodulation for Horn Sets.	IJCAI	1983	DBLP BibTeX RDF
25	Christoph Walther	A many-sorted calculus based on resolution and paramodulation.		1982	RDF
25	Richard Statman	Worst Case Exponential Lower Bounds for Input Resolution with Paramodulation.	SIAM J. Comput.	1980	DBLP DOI BibTeX RDF
25	Chin-Liang Chang	Renamable Paramodulation for Automatic Theorem Proving with Equality.	Artif. Intell.	1970	DBLP DOI BibTeX RDF
15	Kenneth L. McMillan	Quantified Invariant Generation Using an Interpolating Saturation Prover.	TACAS	2008	DBLP DOI BibTeX RDF
15	Maria Paola Bonacina, Nachum Dershowitz	Abstract canonical inference.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	proof orderings, fairness, redundancy, completeness, completion, Inference, saturation, canonicity
15	Reinhold Letz, Gernot Stenz	The Disconnection Tableau Calculus.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	disconnection tableaux, theorem proving
15	Peter Baumgartner 0001, Ulrich Furbach, Björn Pelzer	Hyper Tableaux with Equality.	CADE	2007	DBLP DOI BibTeX RDF
15	Sorin Stratulat	'Descente Infinie' Induction-Based Saturation Procedures.	SYNASC	2007	DBLP DOI BibTeX RDF
15	Harald Ganzinger, Konstantin Korovin	Theory Instantiation.	LPAR	2006	DBLP DOI BibTeX RDF
15	Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron	Tree Automata with Equality Constraints Modulo Equational Theories.	IJCAR	2006	DBLP DOI BibTeX RDF
15	Serge Autexier	The CoRe Calculus.	CADE	2005	DBLP DOI BibTeX RDF
15	Guillem Godoy, Robert Nieuwenhuis	Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups.	Constraints An Int. J.	2004	DBLP DOI BibTeX RDF	symbolic constraints, built-in theories, automated deduction, term orderings
15	Nicolas Peltier	Representing and Building Models for Decidable Subclasses of Equational Clausal Logic.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	resolution, decision procedure, model building, model representation
15	Michael Beeson	Lambda Logic.	IJCAR	2004	DBLP DOI BibTeX RDF
15	Alexandre Riazanov, Andrei Voronkov	Efficient Checking of Term Ordering Constraints.	IJCAR	2004	DBLP DOI BibTeX RDF
15	Harald Ganzinger, Konstantin Korovin	Integrating Equational Reasoning into Instantiation-Based Theorem Proving.	CSL	2004	DBLP DOI BibTeX RDF
15	Christopher Lynch, Barbara Morawska 0001	Automatic Decidability.	LICS	2002	DBLP DOI BibTeX RDF
15	Christopher Lynch, Barbara Morawska 0001	Basic Syntactic Mutation.	CADE	2002	DBLP DOI BibTeX RDF
15	Alexandre Riazanov, Andrei Voronkov	Adaptive Saturation-Based Reasoning.	Ershov Memorial Conference	2001	DBLP DOI BibTeX RDF
15	Maria Paola Bonacina	Combination of Distributed Search and Multi-search in Peers-mcd.d.	IJCAR	2001	DBLP DOI BibTeX RDF
15	Paliath Narendran, Michaël Rusinowitch	The Theory of Total Unary RPO Is Decidable.	Computational Logic	2000	DBLP DOI BibTeX RDF	recursive path ordering, ground reducibility, ordered rewriting, tree automata, first-order theory
15	Ashish Tiwari 0001, Leo Bachmair, Harald Rueß	Rigid E-Unification Revisited.	CADE	2000	DBLP DOI BibTeX RDF