Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Geoff Sutcliffe |
CASC-J4 The 4th IJCAR ATP System Competition. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Adel Bouhoula, Florent Jacquemard |
Automated Induction with Constrained Tree Automata. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
1 | André Platzer, Jan-David Quesel |
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
verification of hybrid systems, decision procedures, computer algebra, automated theorem proving, dynamic logic |
1 | Boris Motik, Ian Horrocks 0001 |
Individual Reuse in Description Logic Reasoning. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Barthe, Benjamin Grégoire, Mariela Pavlova |
Preservation of Proof Obligations from Java to the Java Virtual Machine. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Andrey Paskevich |
Connection Tableaux with Lazy Paramodulation. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Predrag Janicic, Pedro Quaresma |
System Description: GCLCprover + GeoThms. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Jörg Endrullis, Johannes Waldmann, Hans Zantema |
Matrix Interpretations for Proving Termination of Term Rewriting. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Shuvendu K. Lahiri, Madanlal Musuvathi |
Solving Sparse Linear Constraints. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader, Carsten Lutz, Boontawee Suntisrivaraporn |
CEL - A Polynomial-Time Reasoner for Life Science Ontologies. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Yevgeny Kazakov, Boris Motik |
A Resolution-Based Decision Procedure for SHOIQ. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Roy Dyckhoff, Delia Kesner, Stéphane Lengrand |
Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Zimmer, Serge Autexier |
The MathServe System for Semantic Web Reasoning Services. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Kaustuv Chaudhuri, Frank Pfenning, Greg Price |
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Florian Rabe 0001 |
First-Order Logic with Dependent Types. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Benzmüller, Chad E. Brown, Michael Kohlhase |
Cut-Simulation in Impredicative Logics. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Sean McLaughlin |
An Interpretation of Isabelle/HOL in HOL Light. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Chad E. Brown |
Combining Type Theory and Untyped Set Theory. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Sylvie Boldo |
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin Grégoire, Laurent Théry |
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Olga Grinchtein, Martin Leucker, Nir Piterman |
Inferring Network Invariants Automatically. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Beckert, André Platzer |
Dynamic Logic with Non-rigid Functions. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
logical foundations of programming languages, object-orientation, software verification, Dynamic logic, sequent calculus, program logic |
1 | Xiangxue Jia, Jian Zhang 0001 |
A Powerful Technique to Eliminate Isomorphism in Finite Model Search. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
LNH, DASH, scheme, Isomorphism, symmetry breaking |
1 | Geoff Sutcliffe |
CASC-J3 - The 3rd IJCAR ATP System Competition. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Erik Reeber, Warren A. Hunt Jr. |
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Krauss 0001 |
Partial Recursive Functions in Higher-Order Logic. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Christian Urban, Stefan Berghofer |
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
Lambda-calculus, proof assistants, nominal logic, primitive recursion |
1 | Joe Hendrix, José Meseguer 0001, Hitoshi Ohsaki |
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Anna Zamansky, Arnon Avron |
Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Dexter Kozen, Christoph Kreitz, Eva Richter |
Automating Proofs in Category Theory. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Amine Chaieb |
Verifying Mixed Real-Integer Quantifier Elimination. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi |
Specifying and Reasoning About Dynamic Access-Control Policies. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Steven Obua, Sebastian Skalberg |
Importing HOL into Isabelle/HOL. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Allen Van Gelder, Geoff Sutcliffe |
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | David Toman 0001, Grant E. Weddell |
On Keys and Functional Dependencies as First-Class Citizens in Description Logics. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret |
Stratified Context Unification Is NP-Complete. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Assia Mahboubi |
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Hans de Nivelle, Jia Meng |
Geometric Resolution: A Proof Procedure Based on Finite Model Search. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Dale Miller 0001 |
Representing and Reasoning with Operational Semantics. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Stéphane Demri, Denis Lugiez |
Presburger Modal Logic Is PSPACE-Complete. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Roland Zumkeller |
Formal Global Optimisation with Taylor Models. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
Consistency and Completeness of Rewriting in the Calculus of Constructions. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Peter Baumgartner 0001, Renate A. Schmidt |
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Robert L. Constable, Wojciech Moczydlowski |
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Volker Sorge, Andreas Meier 0002, Roy L. McCasland, Simon Colton |
Automatic Construction and Verification of Isotopy Invariants. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Dmitry Tsarkov, Ian Horrocks 0001 |
FaCT++ Description Logic Reasoner: System Description. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Adam Koprowski, Hans Zantema |
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Towards Self-verification of HOL Light. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Ulrich Furbach, Natarajan Shankar (eds.) |
Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Buchberger |
Mathematical Theory Exploration. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin Werner |
On the Strength of Proof-Irrelevant Type Theories. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Giesl, Peter Schneider-Kamp, René Thiemann |
Automatic Termination Proofs in the Dependency Pair Framework. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Brigitte Pientka |
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron |
Tree Automata with Equality Constraints Modulo Equational Theories. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe, Stephan Schulz 0001, Koen Claessen, Allen Van Gelder |
Using the TPTP Language for Writing Derivations and Finite Interpretations. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow, Gertrud Bauer, Paula Schultz |
Flyspeck I: Tame Graphs. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Viorica Sofronie-Stokkermans |
Interpolation in Local Theory Extensions. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Adnan Darwiche |
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation. |
IJCAR |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Yevgeny Kazakov, Hans de Nivelle |
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin, Michaël Rusinowitch (eds.) |
Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar |
The ICS Decision Procedures for Embedded Deduction. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Ewen Denney, Bernd Fischer 0002, Johann Schumann |
Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Guillem Godoy, Ashish Tiwari 0001 |
Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | René Thiemann, Jürgen Giesl, Peter Schneider-Kamp |
Improved Modular Termination Proofs Using Dependency Pairs. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov |
TeMP: A Temporal Monodic Prover. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Anni-Yasmin Turhan, Christian Kissig |
Sonic - Non-standard Inferences Go OilEd. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | K. Subramani 0001 |
Analyzing Selected Quantified Integer Programs. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Michael Beeson |
Lambda Logic. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Schulz 0001 |
System Description: E 0.81. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Miquel Bofill, Albert Rubio |
Redundancy Notions for Paramodulation with Non-monotonic Orderings. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | José Meseguer 0001, Grigore Rosu |
Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Bernd Löchner |
A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Filip Maric, Predrag Janicic |
argo-lib: A Generic Platform for Decision Procedures. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Larchey-Wendling |
Counter-Model Search in Gödel-Dummett Logics. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Tanel Tammet |
Chain Resolution for the Semantic Web. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Boy de la Tour, Mnacho Echenim |
Overlapping Leaf Permutative Equations. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Reinhold Letz, Gernot Stenz |
Generalised Handling of Variables in Disconnection Tableaux. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Simon Colton, Andreas Meier 0002, Volker Sorge, Roy L. McCasland |
Automatic Generation of Classification Theorems for Finite Algebras. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Geoff Sutcliffe, Christian B. Suttner |
The CADE ATP System Competition. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Jeremy Avigad, Kevin Donnelly |
Formalizing O Notation in Isabelle/HOL. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Volker Weispfenning |
Solving Constraints by Elimination Methods. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Ting Zhang 0001, Henny B. Sipma, Zohar Manna |
Decision Procedures for Recursive Data Structures with Integer Constraints. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Jia Meng, Lawrence C. Paulson |
Experiments on Supporting Interactive Proof Using Resolution. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | William M. Farmer |
Formalizing Undefinedness Arising in Calculus. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Graham Steel, Alan Bundy, Monika Maidl |
Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Franz Baader, Silvio Ghilardi, Cesare Tinelli |
A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Winterstein, Alan Bundy, Corin A. Gurr |
Dr.Doodle: A Diagrammatic Theorem Prover. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Riazanov, Andrei Voronkov |
Efficient Checking of Term Ordering Constraints. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Avenhaus |
Efficient Algorithms for Computing Modulo Permutation Theories. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Lutz, Dirk Walther 0002 |
PDL with Negation of Atomic Programs. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann |
Modular Proof Systems for Partial Functions with Weak Equality. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Barthe, Jan Cederquist, Sabrina Tarento |
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Georg Gottlob |
Second-Order Logic over Finite Structures - Report on a Research Programme. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Richard Bonichon |
TaMeD: A Tableau Method for Deduction Modulo. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Àngel J. Gil, Miki Hermann, Gernot Salzer, Bruno Zanuttini |
Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Stuber |
A Model-Based Completeness Proof of Extended Narrowing and Resolution. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Jürgen Avenhaus, Bernd Löchner |
CCE: Testing Ground Joinability. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Alexandre Riazanov, Andrei Voronkov |
Vampire 1.1 (System Description). |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Reiner Hähnle, Neil V. Murray, Erik Rosenthal |
Ordered Resolution vs. Connection Graph Resolution. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|