Search results for "Skolemization"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
74	Matthias Baaz, George Metcalfe	Herbrand Theorems and Skolemization for Prenex Fuzzy Logics.	CiE	2008	DBLP DOI BibTeX RDF	Herbrand Theorem, Fuzzy Logics, Skolemization
47	Philip T. Cox, Tomasz Pietrzykowski	A Complete, Nonredundant Algorithm for Reversed Skolemization.	CADE	1980	DBLP DOI BibTeX RDF
46	Matthias Baaz, Rosalie Iemhoff	Gentzen Calculi for the Existence Predicate.	Stud Logica	2006	DBLP DOI BibTeX RDF	existence predicate, Gentzen calculus, truth-value logics, Gödel logics, Scott logics, cut-elimination, Intuitionistic logic, Kripke models, Skolemization
46	Matthias Baaz, Rosalie Iemhoff	On Interpolation in Existence Logics.	LPAR	2005	DBLP DOI BibTeX RDF	existence predicate, Gentzen calculus, Beth definability, truth-value logics, Gödel logics, Scott logics, interpolation, cut-elimination, Intuitionistic logic, Kripke models, Skolemization
38	Hans de Nivelle	Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms.	CADE	2003	DBLP DOI BibTeX RDF
38	Eugenio G. Omodeo, Jacob T. Schwartz	A 'Theory' Mechanism for a Proof-Verifier Based on First-Order Set Theory.	Computational Logic: Logic Programming and Beyond	2002	DBLP DOI BibTeX RDF
38	Uwe Egly	On the Value of Antiprenexing.	LPAR	1994	DBLP DOI BibTeX RDF
28	Gilles Dowek	Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View.	CoRR	2023	DBLP DOI BibTeX RDF
28	Stefan Hetzl, Jannik Vierling	Induction and Skolemization in saturation theorem proving.	Ann. Pure Appl. Log.	2023	DBLP DOI BibTeX RDF
28	Matthias Baaz, Anela Lolic	Effective Skolemization.	WoLLIC	2023	DBLP DOI BibTeX RDF
28	Matthias Baaz, Anela Lolic	Andrews Skolemization May Shorten Resolution Proofs Non-elementarily.	LFCS	2022	DBLP DOI BibTeX RDF
28	Stefan Hetzl, Jannik Vierling	Induction and Skolemization in saturation theorem proving.	CoRR	2021	DBLP BibTeX RDF
28	Petr Cintula, Denisa Diaconescu, George Metcalfe	Skolemization and Herbrand theorems for lattice-valued logics.	Theor. Comput. Sci.	2019	DBLP DOI BibTeX RDF
28	Martin Diller, Adam Wyner 0001, Hannes Strass	Making Sense of Conflicting (Defeasible) Rules in the Controlled Natural Language ACE: Design of a System with Support for Existential Quantification Using Skolemization.	IWCS (2)	2019	DBLP DOI BibTeX RDF
28	Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller 0001	A proof-theoretic approach to certifying skolemization.	CPP	2019	DBLP DOI BibTeX RDF
28	Alex Kruckman, Nicholas Ramsey	Generic expansion and Skolemization in NSOP1 theories.	Ann. Pure Appl. Log.	2018	DBLP DOI BibTeX RDF
28	Rosalie Iemhoff	On the Existence of Alternative Skolemization Methods.	FLAP	2017	DBLP BibTeX RDF
28	Timm Lampert	A Decision Procedure for Herbrand Formulae without Skolemization.	CoRR	2017	DBLP BibTeX RDF
28	Matthias Baaz, Rosalie Iemhoff	Skolemization in intermediate logics with the finite model property.	Log. J. IGPL	2016	DBLP DOI BibTeX RDF
28	Richard Bonichon, Olivier Hermant	A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization.	CoRR	2015	DBLP BibTeX RDF
28	Petr Cintula, Denisa Diaconescu, George Metcalfe	Skolemization for Substructural Logics.	LPAR	2015	DBLP DOI BibTeX RDF
28	Konstantin Korovin, Margus Veanes	Skolemization Modulo Theories.	ICMS	2014	DBLP DOI BibTeX RDF
28	Guy Van den Broeck, Wannes Meert, Adnan Darwiche	Skolemization for Weighted First-Order Model Counting.	KR	2014	DBLP BibTeX RDF
28	Guy Van den Broeck, Wannes Meert, Adnan Darwiche	Skolemization for Weighted First-Order Model Counting.	CoRR	2013	DBLP BibTeX RDF
28	Kiyoshi Akama, Ekawit Nantajeewarawat	Meaning-preserving Skolemization.	KEOD	2011	DBLP BibTeX RDF
28	Matthias Baaz, George Metcalfe	Herbrand's Theorem, Skolemization and Proof Systems for First-Order Lukasiewicz Logic.	J. Log. Comput.	2010	DBLP DOI BibTeX RDF
28	Claus-Peter Wirth	Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization	CoRR	2009	DBLP BibTeX RDF
28	Matthias Baaz, Rosalie Iemhoff	On Skolemization in constructive theories.	J. Symb. Log.	2008	DBLP DOI BibTeX RDF
28	Matthias Baaz, Rosalie Iemhoff	The Skolemization of existential quantifiers in intuitionistic logic.	Ann. Pure Appl. Log.	2006	DBLP DOI BibTeX RDF
28	Marco Benedetti	Evaluating QBFs via Symbolic Skolemization.	LPAR	2004	DBLP DOI BibTeX RDF
28	Alexander V. Lyaletski	Computer-Oriented Sequent Inferring without Preliminary Skolemization.	IIS	2003	DBLP BibTeX RDF
28	Claus-Peter Wirth	Full First-Order Sequent and Tableau Calculi with Preservation of Solutions and the Liberalized delta-Rule but without Skolemization.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
28	Domenico Cantone, Marianna Nicolosi Asmundo, Eugenio G. Omodeo	Global Skolemization with Grouped Quantifiers.	APPIA-GULP-PRODE	1997	DBLP BibTeX RDF
28	Hans-Jürgen Bürckert, Bernhard Hollunder, Armin Laux	On Skolemization in Constrained Logics.	Ann. Math. Artif. Intell.	1996	DBLP DOI BibTeX RDF
28	Jean Goubault	A BDD-Based Simplification and Skolemization Procedure.	Log. J. IGPL	1995	DBLP DOI BibTeX RDF
28	Matthias Baaz, Alexander Leitsch	On Skolemization and Proof Complexity.	Fundam. Informaticae	1994	DBLP DOI BibTeX RDF
28	Philip T. Cox, Tomasz Pietrzykowski	A Complete, Nonredundant Algorithm for Reversed Skolemization.	Theor. Comput. Sci.	1984	DBLP DOI BibTeX RDF
27	Domenico Cantone, Marianna Nicolosi Asmundo	A Sound Framework for delta-Rule Variants in Free-Variable Semantic Tableaux.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	free-variable semantic tableaux, ?-rule, Skolemization
27	Sandip Ray	Quantification in tail-recursive function definitions.	ACL2	2006	DBLP DOI BibTeX RDF	formal methods, logic, ACL2, conservativity, skolemization
27	Gilles Dowek, Thérèse Hardin, Claude Kirchner	Theorem Proving Modulo.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo
19	Guillaume Burel	Automating Theories in Intuitionistic Logic.	FroCoS	2009	DBLP DOI BibTeX RDF
19	Marc Bezem, Dimitri Hendriks	On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving
19	Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller	Cut Elimination for First Order Gödel Logic by Hyperclause Resolution.	LPAR	2008	DBLP DOI BibTeX RDF
19	Matthias Baaz, George Metcalfe	Proof Theory for First Order Lukasiewicz Logic.	TABLEAUX	2007	DBLP DOI BibTeX RDF
19	Marc Bezem, Thierry Coquand	Automating Coherent Logic.	LPAR	2005	DBLP DOI BibTeX RDF
19	Marco Benedetti	sKizzo: A Suite to Evaluate and Certify QBFs.	CADE	2005	DBLP DOI BibTeX RDF
19	Stefan Brass, Christian Goldberg	Proving the Safety of SQL Queries.	QSIC	2005	DBLP DOI BibTeX RDF	Runtime Errors, SQL, Consistency
19	Stéphane Coulondre	A top-down proof procedure for generalized data dependencies.	Acta Informatica	2003	DBLP DOI BibTeX RDF
19	Arild Waaler, Roger Antonsen	A Free Variable Sequent Calculus with Uniform Variable Splitting.	TABLEAUX	2003	DBLP DOI BibTeX RDF
19	Anatoli Degtyarev, Alexander V. Lyaletski, Marina K. Morokhovets	Evidence Algorithm and Sequent Logical Inference Search.	LPAR	1999	DBLP DOI BibTeX RDF
19	John Harrison 0001	Formalizing Basic First Order Model Theory.	TPHOLs	1998	DBLP DOI BibTeX RDF
19	Andreas Nonnengart, Georg Rock, Christoph Weidenbach	On Generating Small Clause Normal Forms.	CADE	1998	DBLP DOI BibTeX RDF
19	François Bry, Sunna Torge 0001	A Deduction Method Complete for Refutation and Finite Satisfiability.	JELIA	1998	DBLP DOI BibTeX RDF
19	Uwe Egly	Quantifers and the System KE: Some Surprising Results.	CSL	1998	DBLP DOI BibTeX RDF
19	Slim Abdennadher, Heribert Schütz	Model Generation with Existentially Quantified Variables and Constraints.	ALP/HOA	1997	DBLP DOI BibTeX RDF
19	Natarajan Shankar	Proof Search in the Intuitionistic Sequent Calculus.	CADE	1992	DBLP DOI BibTeX RDF
19	Matthias Baaz, Alexander Leitsch	A Strong Problem Reduction Method Based on Function Introduction.	ISSAC	1990	DBLP DOI BibTeX RDF
19	D. Duchier, Drew V. McDermott	LOGICALC: An Environment for Interactive Proof Development.	CADE	1988	DBLP DOI BibTeX RDF
19	Jieh Hsiang, Mandayam K. Srivas	PROLOG-Based Inductive Theorem Proving.	FSTTCS	1985	DBLP DOI BibTeX RDF