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 |
|