Search results for "proof-search"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
70	Didier Galmiche, J.-M. Notin	Proof-search and proof nets in Mixed Linear Logic.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
63	Sachio Hirokawa, Daisuke Nagano	Long Normal Form Proof Search and Counter-Model Generation.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
63	David J. Pym	Notes Towards a Semantics for Proof-search.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
51	Didier Galmiche (eds.)	Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics 2000, held in conjunction with CADE-17 Conference, Pittsburgh, PA, USA, June 20-21, 2000	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP BibTeX RDF
51	Nikos Mylonakis	Proof assistance for refinement in type theory.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
51	Aleksey Nogin	Writing Constructive Proofs Yielding Efficient Extracted Programs.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
51	Didier Galmiche	Preface.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
51	James Harland, David J. Pym, Michael Winikoff	Forward and Backward Chaining in Linear Logic.	Workshop on Type-Theoretic Languages: Proof Search and Semantics	2000	DBLP DOI BibTeX RDF
51	Didier Galmiche (eds.)	Workshop on Proof Search in Type-Theoretic Languages (in conjunction with CADE-15 Conference), Lindau, Germany, July 5, 1998	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP BibTeX RDF
51	David J. Pym	Logic Programming with Bunched Implications.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Uwe Egly, Stephan Schmitt	Intuitionistic Proof Transformations: Complexity and Applications.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Michael Franssen	Embedding First-Order Tableaux into a Pure Type System.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Frank Pfenning, Carsten Schürmann	Algorithms for Equality and Unification in the Presence of Notational Definitions.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Didier Galmiche	Preface.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Didier Galmiche, Bruno Martin	Proof nets Construction and Automated Deduction in Non-Commutative Linear Logic.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Luís Pinto 0001, Roy Dyckhoff	Sequent Calculi for the Normal Terms of the - and - Calculi.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
51	Dominique Larchey-Wendling, Didier Galmiche	Provability in Intuitionistic Linear Logic from a New Interpretation on Petri nets.	Proof Search in Type-Theoretic Languages@CADE	1998	DBLP DOI BibTeX RDF
42	Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002	Proof Search and Proof Check for Equational and Inductive Theorems.	CADE	2003	DBLP DOI BibTeX RDF	proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant
41	Alexis Saurin	Towards Ludics Programming: Interactive Proof Search.	ICLP	2008	DBLP DOI BibTeX RDF	Ludics, Proof Normalization, Interaction, Logic Programming, Game Semantics, Proof Search
37	David J. Pym, Lincoln A. Wallen	Investigations into Proof-Search in a System of First-Order Dependent Function Types.	CADE	1990	DBLP DOI BibTeX RDF
32	Jean-Marc Andreoli	Focussing Proof-Net Construction as a Middleware Paradigm.	CADE	2002	DBLP DOI BibTeX RDF	Proof construction, Focussing, Middleware, Transactions, Proof search, Proof-nets
32	Dale Miller 0001, Alexis Saurin	From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic.	CSL	2007	DBLP DOI BibTeX RDF
31	Herman Geuvers, Erik Poll, Jan Zwanenburg	Safe Proof Checking in Type Theory with Y.	CSL	1999	DBLP DOI BibTeX RDF
31	Andrew Ireland, Jamie Stark	Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis.	Autom. Softw. Eng.	2006	DBLP DOI BibTeX RDF	partial order planning, deductive synthesis, program synthesis, proof planning
31	L. Habert, J.-M. Notin, Didier Galmiche	LINK: A Proof Environment Based on Proof Nets.	TABLEAUX	2002	DBLP DOI BibTeX RDF
29	Chuck C. Liang, Dale Miller 0001	Focusing and Polarization in Intuitionistic Logic.	CSL	2007	DBLP DOI BibTeX RDF
27	Martin Fränzle, Christian Herde	Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems.	LPAR	2003	DBLP DOI BibTeX RDF	non-clausal propositional logic, zero-one linear constraint systems, Satisfiability, proof search, acceleration techniques
27	Andrei Voronkov	How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	theorem proving, modal logic, description logics, proof-search, inverse method
27	Luís Caires, Luís Monteiro	Proof Net Semantics of Proof Search Computation.	ALP/HOA	1997	DBLP DOI BibTeX RDF
26	David Baelde, Dale Miller 0001	Least and Greatest Fixed Points in Linear Logic.	LPAR	2007	DBLP DOI BibTeX RDF
24	John Harrison 0001	Optimizing Proof Search in Model Elimination.	CADE	1996	DBLP DOI BibTeX RDF
24	Luís Pinto 0001, Tarmo Uustalu	Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents.	TABLEAUX	2009	DBLP DOI BibTeX RDF
24	Joachim Posegga	Compiling Proof Search in Semantic Tableaux.	ISMIS	1993	DBLP DOI BibTeX RDF
23	Mihhail Matskin, Enn Tyugu	Strategies of Structural Synthesis of Programs.	ASE	1997	DBLP DOI BibTeX RDF	structural program synthesis strategies, deductive program synthesis method, compositional programming, decidable logical calculus, PSPACE complexity, independent subtasks, iteration synthesis, regular data structures, heuristics, programming environments, structured programming, proof search, search efficiency
23	Raúl Monroy	Concept Formation via Proof Planning Failure.	LPAR	2001	DBLP DOI BibTeX RDF
23	Vivek Nigam, Dale Miller 0001	Algorithmic specifications in linear logic with subexponentials.	PPDP	2009	DBLP DOI BibTeX RDF	subexponentials, linear logic, proof search
23	Clemens Grabmayer	Using Proofs by Coinduction to Find "Traditional" Proofs.	CALCO	2005	DBLP DOI BibTeX RDF
21	Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer	System Description: inka 5.0 - A Logic Voyager.	CADE	1999	DBLP DOI BibTeX RDF
21	Helmut Schwichtenberg	Proof Search in Minimal Logic.	AISC	2004	DBLP DOI BibTeX RDF
21	Paola Bruscoli, Alessio Guglielmi	On Structuring Proof Search for First Order Linear Logic.	LPAR	2003	DBLP DOI BibTeX RDF
21	Paola Bruscoli	A Purely Logical Account of Sequentiality in Proof Search.	ICLP	2002	DBLP DOI BibTeX RDF
21	Didier Galmiche, Daniel Méry	Connection-Based Proof Search in Propositional BI Logic.	CADE	2002	DBLP DOI BibTeX RDF
21	Raul H. C. Lopes	Automatic Generation of Proof Search Strategies for Second-order Logic.	CADE	1999	DBLP DOI BibTeX RDF
21	Christian Urban	Implementation of Proof Search in the Imperative Programming Language Pizza.	TABLEAUX	1998	DBLP DOI BibTeX RDF	Success Continuations, G4ip, Pizza
20	Elaine Pimentel, Dale Miller 0001	On the Specification of Sequent Systems.	LPAR	2005	DBLP DOI BibTeX RDF
20	Dale Miller 0001, Vivek Nigam	Incorporating Tables into Proofs.	CSL	2007	DBLP DOI BibTeX RDF
20	Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel	KIV 3.0 for Provably Correct Systems.	FM-Trends	1998	DBLP DOI BibTeX RDF
19	Matthew Bishop	A Breadth-First Strategy for Mating Search.	CADE	1999	DBLP DOI BibTeX RDF
19	Dominique Larchey-Wendling, Daniel Méry, Didier Galmiche	STRIP: Structural Sharing for Efficient Proof-Search.	IJCAR	2001	DBLP DOI BibTeX RDF
19	Didier Galmiche, Daniel Méry	Proof-Search and Countermodel Generation in Propositional BI Logic.	TACS	2001	DBLP DOI BibTeX RDF
19	Didier Galmiche	Workshop: Type-Theoretic Languages: Proof-Search and Semantics.	CADE	2000	DBLP DOI BibTeX RDF
19	Hiu Fai Chau	A Proof Search System for a Modal Substructural Logic Based on Labelled Deductive Systems.	LPAR	1993	DBLP DOI BibTeX RDF
19	Zhe Hou, Rajeev Goré, Alwen Tiu	A labelled sequent calculus for BBI: proof theory and proof search.	J. Log. Comput.	2018	DBLP DOI BibTeX RDF
19	Ekaterina Komendantskaya, Patricia Johann	Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic.	CoRR	2015	DBLP BibTeX RDF
19	Zhe Hou, Alwen Tiu, Rajeev Goré	A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search	CoRR	2013	DBLP BibTeX RDF
19	Zhe Hou, Alwen Tiu, Rajeev Goré	A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search.	TABLEAUX	2013	DBLP DOI BibTeX RDF
19	David J. Pym, Eike Ritter	Reductive logic and proof-search - proof theory, semantics, and control.		2004	RDF
19	Natarajan Shankar	Using Proof Theory to Optimize Proof Search.	ICLP Workshop: Proof-Theoretical Extensions on Logic Programming	1994	DBLP BibTeX RDF
19	Lincoln A. Wallen	Automated proof search in non-classical logics - efficient matrix proof methods for modal and intuitionistic logics.		1990	RDF
18	Andrei Voronkov	How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi.	LICS	2000	DBLP DOI BibTeX RDF
17	Matthew Bishop, Peter B. Andrews	Selectively Instantiating Definitions.	CADE	1998	DBLP DOI BibTeX RDF
17	Jason Hickey, Aleksey Nogin	Fast Tactic-Based Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
17	Jean Goubault	The Complexity of Resource-Bounded First-Order Classical Logic.	STACS	1994	DBLP DOI BibTeX RDF	Topics computational complexity, computational issues in AI (automated theorem proving), logics
17	Rajeev Goré, Linda Postniece, Alwen Tiu	Taming Displayed Tense Logics Using Nested Sequents with Deep Inference.	TABLEAUX	2009	DBLP DOI BibTeX RDF
17	Andrew Cook, Andrew Ireland, Greg Michaelson, Norman Scaife	Discovering applications of higher order functions through proof planning.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF
17	Jürgen Schmidhuber	Completely Self-referential Optimal Reinforcement Learners.	ICANN (2)	2005	DBLP DOI BibTeX RDF
17	Fredrik Lindblad, Marcin Benke	A Tool for Automated Theorem Proving in Agda.	TYPES	2004	DBLP DOI BibTeX RDF
17	Jean-Marc Andreoli, Roberto Maieli	Fucusing and Proof-Nets in Linear and Non-commutative Logic.	LPAR	1999	DBLP DOI BibTeX RDF
16	Alwen Fernanto Tiu	Model Checking for pi-Calculus Using Proof Search.	CONCUR	2005	DBLP DOI BibTeX RDF
16	Dale Miller 0001	Higher-Order Quantification and Proof Search.	AMAST	2002	DBLP DOI BibTeX RDF
16	Dominique Larchey-Wendling	Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic.	CADE	2002	DBLP DOI BibTeX RDF
16	Joshua S. Hodas, Pablo López, Jeffrey Polakow, Lubomira Stoilova, Ernesto Pimentel 0001	A Tag-Frame System of Resource Management for Proof Search in Linear-Logic Programming.	CSL	2002	DBLP DOI BibTeX RDF
16	Amy P. Felty	Proof Search with Set Variable Instantiation in the Calculus of Constructions.	CADE	1996	DBLP DOI BibTeX RDF
16	Andrei Voronkov	A proof-search method for the first-order logic.	Conference on Computer Logic	1988	DBLP DOI BibTeX RDF
16	Quoc Bao Vo	A task-oriented agent-based mechanism for theorem proving.	IAT	2003	DBLP DOI BibTeX RDF
16	Stephan Schulz 0001	Learning Search Control Knowledge for Equational Theorem Proving.	KI/ÖGAI	2001	DBLP DOI BibTeX RDF
15	Claudio Castellini, Alan Smaill	Proof Planning for First-Order Temporal Logic.	CADE	2005	DBLP DOI BibTeX RDF
15	Alexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine	Theorem Proving and Proof Verification in the System SAD.	MKM	2004	DBLP DOI BibTeX RDF
15	Dale Miller 0001, Elaine Pimentel	Using Linear Logic to Reason about Sequent Systems.	TABLEAUX	2002	DBLP DOI BibTeX RDF
15	Andrew Gacek	Relating nominal and higher-order abstract syntax specifications.	PPDP	2010	DBLP DOI BibTeX RDF	higher-order abstract syntax, proof search, nominal logic
15	Andrew Gacek, Dale Miller 0001, Gopalan Nadathur	Combining Generic Judgments with Recursive Definitions.	LICS	2008	DBLP DOI BibTeX RDF	generic judgments, reasoning about operational semantics, higher-order abstract syntax, proof search
15	Dale Miller 0001	Collection analysis for Horn clause programs.	PPDP	2006	DBLP DOI BibTeX RDF	static analysis, linear logic, Horn clauses, proof search
15	Dale Miller 0001, Alwen Tiu	A proof theory for generic judgments.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	?-tree syntax, ?-quantifier, generic judgments, reasoning about operational semantics, higher-order abstract syntax, Proof search
15	James Harland, David J. Pym	Resource-distribution via Boolean constraints.	ACM Trans. Comput. Log.	2003	DBLP DOI BibTeX RDF	Boolean constraints, Algebras, sequent calculus, substructural logics, proof-search, relevant logics
15	Dale Miller 0001, Alwen Fernanto Tiu	A Proof Theory for Generic Judgments: An extended abstract.	LICS	2003	DBLP DOI BibTeX RDF	reasoning about operational semantics, generic judgments, higher-order abstract syntax, proof search
15	Claudia Faggian	Proof construction and non-commutativity: a cluster calculus.	PPDP	2000	DBLP DOI BibTeX RDF	non-commutative logic, logic programming, linear logic, proof search, focalization
15	Sergei G. Vorobyov	A structural completeness theorem for a class of conditional rewrite rule systems.	Conference on Computer Logic	1988	DBLP DOI BibTeX RDF	conditional rewrite rules, case splitting, finite termination, reduction, inference rules, confluency, proof search, decision algorithms, strong completeness
14	Linda Postniece	Deep Inference in Bi-intuitionistic Logic.	WoLLIC	2009	DBLP DOI BibTeX RDF
14	Geng-Dian Huang, Bow-Yaw Wang	Complete SAT-Based Model Checking for Context-Free Processes.	ATVA	2007	DBLP DOI BibTeX RDF
14	Tatjana Lutovac, James Harland	A Redundancy Analysis of Sequent Proofs.	TABLEAUX	2005	DBLP DOI BibTeX RDF
14	Jürgen Schmidhuber	Ultimate Cognition à la Gödel.	Cogn. Comput.	2009	DBLP DOI BibTeX RDF	Universal cognitive systems, Ultimate cognition, Optimal general problem solver, Goedel machine, Global optimality theorem, AI becoming a formal science, Self-reference
14	Adam Chlipala	A certified type-preserving compiler from lambda calculus to assembly language.	PLDI	2007	DBLP DOI BibTeX RDF	denotational semantics, dependent types, compiler verification, interactive proof assistants
14	Mads Dam	Decidability and proof systems for language-based noninterference relations.	POPL	2006	DBLP DOI BibTeX RDF	intransitive noninterference, information flow, language-based security, noninterference, multi-level security
14	Dexter Kozen, Christoph Kreitz, Eva Richter	Automating Proofs in Category Theory.	IJCAR	2006	DBLP DOI BibTeX RDF
14	Serge Autexier, Dominik Dietrich	Synthesizing Proof Planning Methods and Omega-Ants Agents from Mathematical Knowledge.	MKM	2006	DBLP DOI BibTeX RDF
14	Martin Hofmann 0001	Proof-Theoretic Approach to Description-Logic.	LICS	2005	DBLP DOI BibTeX RDF
14	Alexander Leitsch	Decision Procedures and Model Building, or How to Improve Logical Information in Automated Deduction.	FTP (LNCS Selection)	1998	DBLP DOI BibTeX RDF
12	Grigori Mints	Unwinding a Non-effective Cut Elimination Proof.	CSR	2006	DBLP DOI BibTeX RDF
12	Christian Urban, James Cheney	Avoiding Equivariance in Alpha-Prolog.	TLCA	2005	DBLP DOI BibTeX RDF
12	Richard Bonichon	TaMeD: A Tableau Method for Deduction Modulo.	IJCAR	2004	DBLP DOI BibTeX RDF