BibSLEIGH — first-order tag

first-order

first-order

Tag #first-order

329 papers:

CC-2020-Castro-PerezY #compilation #parallel: Compiling first-order functions to session-typed parallel code (DCP, NY), pp. 143–154.
CSL-2020-GrangeS #invariant #logic: Order-Invariant First-Order Logic over Hollow Trees (JG, LS), p. 16.
FSCD-2019-HeijltjesHS #linear #logic #proving: Proof Nets for First-Order Additive Linear Logic (WH, DJDH, LS), p. 22.
ICML-2019-LeeW #algorithm #performance #problem: First-Order Algorithms Converge Faster than $O(1/k)$ on Convex Problems (CPL, SW), pp. 3754–3762.
ICML-2019-Simon-GabrielOB #network: First-Order Adversarial Vulnerability of Neural Networks and Input Dimension (CJSG, YO, LB, BS, DLP), pp. 5809–5817.
ECOOP-2019-WattMKG #encapsulation #logic: A Program Logic for First-Order Encapsulated WebAssembly (CW, PM, NRK, PG), p. 30.
PADL-2019-Lierler #equivalence #logic programming #source code: Strong Equivalence and Program's Structure in Arguing Essential Equivalence Between First-Order Logic Programs (YL), pp. 1–18.
SAS-2019-0001NIU #fixpoint #logic #source code #verification: Temporal Verification of Programs via First-Order Fixpoint Logic (NK0, TN, AI, HU0), pp. 413–436.
CAV-2019-IosifX #automaton: Alternating Automata Modulo First Order Theories (RI, XX), pp. 43–63.
DLT-2018-Michielini #finite #logic #problem #word: Uniformization Problem for Variants of First Order Logic over Finite Words (VM), pp. 516–528.
ICML-2018-0001MPS #approximate #on the: On the Limitations of First-Order Approximation in GAN Dynamics (JL0, AM, JP, LS), pp. 3011–3019.
ICML-2018-Allen-ZhuBL #bound: Make the Minority Great Again: First-Order Regret Bound for Contextual Bandits (ZAZ, SB, YL), pp. 186–194.
ICML-2018-OstrovskiiH #adaptation #algorithm #performance: Efficient First-Order Algorithms for Adaptive Signal Denoising (DO, ZH), pp. 3943–3952.
ICML-2018-SewardUBJH #generative #network: First Order Generative Adversarial Networks (CS, TU, UB, NJ, SH), pp. 4574–4583.
ICML-2018-TaylorSL #automation #convergence: Lyapunov Functions for First-Order Methods: Tight Automated Convergence Guarantees (AT, BVS, LL), pp. 4904–4913.
LOPSTR-2018-Lucas #proving #satisfiability: Proving Program Properties as First-Order Satisfiability (SL), pp. 3–21.
POPL-2018-PadonHLPSS #liveness #logic #safety: Reducing liveness to safety in first-order logic (OP, JH, GL, AP, MS, SS), p. 33.
ASE-2018-BrunelCCM #model checking #relational #specification: The electrum analyzer: model checking relational first-order temporal specifications (JB, DC, AC, NM), pp. 884–887.
ESEC-FSE-2018-ErataGKT #automation #logic #named #reasoning #relational: AlloyInEcore: embedding of first-order relational logic into meta-object facility for automated model reasoning (FE, AG, IK, BT), pp. 920–923.
CASE-2018-ZhaoCCPLG #lightweight #named: FLUIDS: A First-Order Lightweight Urban Intersection Driving Simulator (HZ, AC, SAC, BP, ML, KG), pp. 697–704.
IJCAR-2018-ClaessenS #encoding #equation #logic #performance: Efficient Encodings of First-Order Horn Formulas in Equational Logic (KC, NS), pp. 388–404.
IJCAR-2018-JeannerodT #algebra: Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (NJ, RT), pp. 439–454.
DLT-2017-LodayaS #complexity #logic #quantifier: Two-Variable First Order Logic with Counting Quantifiers: Complexity Results (KL, AVS), pp. 260–271.
IFM-2017-ChenF #proving #verification: Triggerless Happy - Intermediate Verification with a First-Order Prover (YC, CAF), pp. 295–311.
ICML-2017-WangX #algorithm: Exploiting Strong Convexity from Data with Primal-Dual First-Order Algorithms (JW, LX), pp. 3694–3702.
LOPSTR-2017-Ait-KaciP #fuzzy #unification: Fuzzy Unification and Generalization of First-Order Terms over Similar Signatures (HAK, GP), pp. 218–234.
LOPSTR-2017-Lucas #analysis: Analysis of Rewriting-Based Systems as First-Order Theories (SL), pp. 180–197.
CASE-2017-YamazakiNS #abstraction #composition #hybrid #petri net #problem: A decomposition method with discrete abstraction for simultaneous traffic signal control and route selection problem with first-order hybrid Petri Nets (RY, TN, SS), pp. 352–357.
CADE-2017-0001SUP #consistency #detection #knowledge base #nondeterminism #scalability: Detecting Inconsistencies in Large First-Order Knowledge Bases (SS0, GS, JU, AP), pp. 310–325.
CADE-2017-Kiesl0 #logic: A Unifying Principle for Clause Elimination in First-Order Logic (BK, MS0), pp. 274–290.
CADE-2017-TeuckeW #constraints #decidability #linear #monad: Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints (AT, CW), pp. 202–219.
CSL-2017-ChenFH #bound #logic #quantifier #rank #slicing: Slicewise Definability in First-Order Logic with Bounded Quantifier Rank (YC, JF, XH), p. 16.
CSL-2017-Kovacs #proving: First-Order Interpolation and Grey Areas of Proofs (Invited Talk) (LK), p. 1.
CSL-2017-Kreutzer #model checking #roadmap: Current Trends and New Perspectives for First-Order Model Checking (Invited Talk) (SK), p. 5.
CSL-2017-VerbitskyZ #complexity #morphism #on the: On the First-Order Complexity of Induced Subgraph Isomorphism (OV, MZ), p. 16.
FSCD-2016-BenkeSC #functional #logic #source code #synthesis: Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic (MB, AS, DWC), p. 16.
FSCD-2016-RappM #automation #linear #term rewriting: Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems (FR, AM), p. 12.
ICML-2016-ArjevaniS #algorithm #complexity #on the #optimisation: On the Iteration Complexity of Oblivious First-Order Optimization Algorithms (YA, OS), pp. 908–916.
MoDELS-2016-DaniaC #constraints #logic #named #ocl #satisfiability: OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints (CD, MC), pp. 65–75.
PPDP-2016-GreweERM #compilation #logic #specification: Exploration of language specifications by compilation to first-order logic (SG, SE, MR, MM), pp. 104–117.
CSL-2016-EickmeyerK #graph #invariant #logic: Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs (KE, KiK), p. 15.
PODS-2015-BeameBGS #symmetry: Symmetric Weighted First-Order Model Counting (PB, GVdB, EG, DS), pp. 313–328.
FM-2015-SchmittU #axiom #logic: Axiomatization of Typed First-Order Logic (PHS, MU), pp. 470–486.
ICFP-2015-AvanziniLM #complexity #functional #higher-order #source code: Analysing the complexity of functional programs: higher-order meets first-order (MA, UDL, GM), pp. 152–164.
ICML-2015-ZhouZS #analysis #bound #convergence #fault: ℓ₁_,p-Norm Regularization: Error Bounds and Convergence Rate Analysis of First-Order Methods (ZZ, QZ, AMCS), pp. 1501–1510.
PEPM-2015-AsadaS0 #functional #refinement #relational #source code #verification: Verifying Relational Properties of Functional Programs by First-Order Refinement (KA, RS, NK), pp. 61–72.
FoSSaCS-2015-SchubertUZ #logic #on the: On the Mints Hierarchy in First-Order Intuitionistic Logic (AS, PU, KZ), pp. 451–465.
CADE-2015-GorznyP #proving #towards: Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses (JG, BWP), pp. 356–366.
CADE-2015-Plaisted #automation #deduction: History and Prospects for First-Order Automated Deduction (DAP), pp. 3–28.
CSL-2015-BovaM #finite #query: First-Order Queries on Finite Abelian Groups (SB, BM), pp. 41–59.
CSL-2015-ClementeL #analysis #automaton #reachability: Reachability Analysis of First-order Definable Pushdown Systems (LC, SL), pp. 244–259.
CSL-2015-MogaveroP #logic: Binding Forms in First-Order Logic (FM, GP), pp. 648–665.
CSL-2015-Paperman #logic: Finite-Degree Predicates and Two-Variable First-Order Logic (CP), pp. 616–630.
LICS-2015-GradelPSK #polynomial: Characterising Choiceless Polynomial Time with First-Order Interpretations (EG, WP, SS, LK), pp. 677–688.
PODS-2014-DurandSS #database #query: Enumerating answers to first-order queries over databases of low degree (AD, NS, LS), pp. 121–131.
ICALP-v2-2014-Jancar #bisimulation #equivalence: Bisimulation Equivalence of First-Order Grammars (PJ), pp. 232–243.
ICALP-v2-2014-JungLGS #logic #probability: Monodic Fragments of Probabilistic First-Order Logic (JCJ, CL, SG, LS), pp. 256–267.
ICALP-v2-2014-PlaceZ #quantifier #word: Going Higher in the First-Order Quantifier Alternation Hierarchy on Words (TP, MZ), pp. 342–353.
RTA-TLCA-2014-FuhsK: First-Order Formative Rules (CF, CK), pp. 240–256.
ICFP-2014-Winograd-CortH #how: Settable and non-interfering signal functions for FRP: how a first-order switch is more than enough (DWC, PH), pp. 213–225.
LCT-NLE-2014-PaisT #deduction #logic #novel #proving: Novel Didactic Proof Assistant for First-Order Logic Natural Deduction (JP, AT), pp. 441–451.
ICML-c1-2014-MeiZZ #logic #modelling #robust: Robust RegBayes: Selectively Incorporating First-Order Logic Domain Knowledge into Bayesian Models (SM, JZ, JZ), pp. 253–261.
KR-2014-AsuncionZZ #logic programming #semantics #source code: Logic Programs with Ordered Disjunction: First-Order Semantics and Expressiveness (VA, YZ, HZ).
KR-2014-BroeckMD: Skolemization for Weighted First-Order Model Counting (GVdB, WM, AD).
KR-2014-Lin #formal method #linear #logic #source code: A Formalization of Programs in First-Order Logic with a Discrete Linear Order (FL).
KR-2014-Lin14a #axiom #higher-order #induction #semantics: A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations (FL).
KR-2014-Zhou #logic #revisited: First-Order Default Logic Revisited (YZ).
ASPLOS-2014-BornholtMM #named #nondeterminism: Uncertain: a first-order type for uncertain data (JB, TM, KSM), pp. 51–66.
STOC-2014-GroheKS #graph: Deciding first-order properties of nowhere dense graphs (MG, SK, SS), pp. 89–98.
CAV-2014-Voronkov #architecture #named #proving #theorem proving: AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
IJCAR-2014-Otten #logic #named #proving: MleanCoP: A Connection Prover for First-Order Modal Logic (JO), pp. 269–276.
LICS-CSL-2014-Chen #query #set: The tractability frontier of graph-like first-order query sets (HC), p. 9.
LICS-CSL-2014-PlaceZ #logic #regular expression: Separating regular languages with first-order logic (TP, MZ), p. 10.
LICS-CSL-2014-Williams #graph #performance: Faster decision of first-order graph properties (RW), p. 6.
PODS-2013-KazanaS #bound #query: Enumeration of first-order queries on classes of structures with bounded expansion (WK, LS), pp. 297–308.
ITiCSE-2013-KyrilovN #assessment #automation #information management #logic #representation: Automatic formative assessment of exercises on knowledge representation in first-order logic (AK, DCN), p. 343.
ICML-c3-2013-Mairal #optimisation: Optimization with First-Order Surrogate Functions (JM), pp. 783–791.
SEKE-2013-WangKWN #case study #feature model #metric #statistics: A Study on First Order Statistics-Based Feature Selection Techniques on Software Metric Data (HW, TMK, RW, AN), pp. 467–472.
CADE-2013-BlanchetteP #morphism #named #polymorphism: TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism (JCB, AP), pp. 414–420.
CADE-2013-ChihaniMR #logic #proving: Foundational Proof Certificates in First-Order Logic (ZC, DM, FR), pp. 162–177.
CADE-2013-KersaniP #decidability: Completeness and Decidability Results for First-Order Clauses with Indices (AK, NP), pp. 58–75.
CAV-2013-KovacsV #proving #theorem proving: First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
CSL-2013-HampsonK #linear #logic: One-variable first-order linear temporal logics with counting (CH, AK), pp. 348–362.
CSL-2013-HarwathS #invariant #locality #logic #on the #quantifier: On the locality of arb-invariant first-order logic with modulo counting quantifiers (FH, NS), pp. 363–379.
LICS-2013-EickmeyerKK #graph #invariant #logic #model checking: Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes (KE, KiK, SK), pp. 134–142.
LICS-2013-Halpern #logic #proving #security #using: From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic (JYH), pp. 2–3.
ICALP-v2-2012-GavenciakKO: Deciding First Order Properties of Matroids (TG, DK, SiO), pp. 239–250.
PPDP-2012-BacciCFV #automation #source code #specification #synthesis: Automatic synthesis of specifications for first order curry programs (GB, MC, MAF, AV), pp. 25–34.
ESOP-2012-LeeOCY #framework #named: GMeta: A Generic Formal Metatheory Framework for First-Order Representations (GL, BCdSO, SC, KY), pp. 436–455.
FoSSaCS-2012-BoveDS #automation #functional #interactive #reasoning #source code: Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs (AB, PD, ASR), pp. 104–118.
FoSSaCS-2012-Kartzow #automaton #exponential #model checking: First-Order Model Checking on Nested Pushdown Trees is Complete for Doubly Exponential Alternating Time (AK), pp. 376–390.
CSL-2012-HetzlS #logic: Herbrand-Confluence for Cut Elimination in Classical First Order Logic (SH, LS), pp. 320–334.
CSL-2012-KuusistoMV #decidability #geometry: Undecidable First-Order Theories of Affine Geometries (AK, JM, JV), pp. 470–484.
ICST-2012-KintisPM #higher-order: Isolating First Order Equivalent Mutants via Second Order Mutation (MK, MP, NM), pp. 701–710.
IJCAR-2012-RathsO #library #logic #problem: The QMLTP Problem Library for First-Order Modal Logics (TR, JO), pp. 454–461.
LICS-2012-ElberfeldGT #higher-order #logic #monad: Where First-Order and Monadic Second-Order Logic Coincide (ME, MG, TT), pp. 265–274.
LICS-2012-EngelmannKS #higher-order #model checking #monad: First-Order and Monadic Second-Order Model-Checking on Ordered Structures (VE, SK, SS), pp. 275–284.
LICS-2012-GollerJL #complexity: The Complexity of Decomposing Modal and First-Order Theories (SG, JCJ, ML), pp. 325–334.
LICS-2012-Jancar #decidability #equivalence: Decidability of DPDA Language Equivalence via First-Order Grammars (PJ), pp. 415–424.
LICS-2012-KieronskiMPT #equivalence #logic: Two-Variable First-Order Logic with Equivalence Closure (EK, JM, IPH, LT), pp. 431–440.
LICS-2012-KrebsS: Non-definability of Languages by Generalized First-order Formulas over (N, +) (AK, AVS), pp. 451–460.
ICALP-v2-2011-AndersonMSS #invariant #locality #logic #query: Locality of Queries Definable in Invariant First-Order Logic with Arbitrary Built-in Predicates (MA, DvM, NS, LS), pp. 368–379.
RTA-2011-GasconMR #unification: First-Order Unification on Compressed Terms (AG, SM, LR), pp. 51–60.
OOPSLA-2011-PuBS #algorithm #programming #synthesis: Synthesis of first-order dynamic programming algorithms (YP, RB, SS), pp. 83–98.
CASE-2011-DotoliFI #hybrid #petri net: A freeway traffic control model by first order hybrid Petri nets (MD, MPF, GI), pp. 425–431.
CADE-2011-Claessen #automation #logic #reasoning: The Anatomy of Equinox — An Extensible Automated Reasoning Tool for First-Order Logic and Beyond — (KC), pp. 1–3.
CADE-2011-ClaessenLS #logic: Sort It Out with Monotonicity — Translating between Many-Sorted and Unsorted First-Order Logic (KC, AL, NS), pp. 207–221.
CADE-2011-SchneiderS #automation #ontology #owl #proving #reasoning #theorem proving #using: Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.
CSL-2011-Eickmeyer #logic #random: Non-Definability Results for Randomised First-Order Logic (KE), pp. 218–232.
LICS-2011-BarrasJSW #decidability #higher-order #named #type system: CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory (BB, JPJ, PYS, QW), pp. 143–151.
LICS-2011-Krokhin #complexity: The Complexity of Evaluating First-Order Sentences over a Fixed Structure (AAK), p. 331.
LICS-2011-MadelaineM #logic #similarity: A Tetrachotomy for Positive First-Order Logic without Equality (FRM, BM), pp. 311–320.
PODS-2010-Wijsen #database #nondeterminism #on the #query: On the first-order expressibility of computing certain answers to conjunctive queries over uncertain databases (JW), pp. 179–190.
LATA-2010-CabessaV #classification #network: A Hierarchical Classification of First-Order Recurrent Neural Networks (JC, AEPV), pp. 142–153.
LATA-2010-JordanZ #quantifier: Untestable Properties Expressible with Four First-Order Quantifiers (CJ, TZ), pp. 333–343.
KR-2010-BelardinelliL #interactive #logic #multi: Interactions between Time and Knowledge in a First-order Logic for Multi-Agent Systems (FB, AL).
LOPSTR-2010-BacciC #functional #logic programming #source code: Abstract Diagnosis of First Order Functional Logic Programs (GB, MC), pp. 215–233.
LOPSTR-2010-CalvesF: The First-Order Nominal Link (CC, MF), pp. 234–248.
PADL-2010-Perera #interactive #programming: First-Order Interactive Programming (RP), pp. 186–200.
ESOP-2010-NaumannB #bound #higher-order #information management: Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (DAN, AB), pp. 2–22.
CAV-2010-BasinKM #logic #monitoring #policy: Policy Monitoring in First-Order Temporal Logic (DAB, FK, SM), pp. 1–18.
CSL-2010-MartinM #complexity #logic #similarity: The Complexity of Positive First-Order Logic without Equality II: The Four-Element Case (BM, JM), pp. 426–438.
ICTSS-2010-Gladisch #generative #logic #quantifier #source code #specification #testing: Test Data Generation for Programs with Quantified First-Order Logic Specifications (CG), pp. 158–173.
LICS-2010-He #finite #on the #quantifier #strict: On the Strictness of the First-Order Quantifier Structure Hierarchy over Finite Structures (YH), pp. 170–178.
TAP-2010-AhnD #axiom #logic #testing #verification: Testing First-Order Logic Axioms in Program Verification (KYA, ED), pp. 22–37.
EDM-2009-Barker-PlummerCD #logic #natural language: Dimensions of Difficulty in Translating Natural Language into First-Order Logic (DBP, RC, RD), pp. 220–229.
ICPC-2009-LinsteadHLB #java #markov #modelling: Capturing Java naming conventions with first-order Markov models (EL, LH, CVL, PB), pp. 313–314.
ICEIS-DISI-2009-AmiratO #architecture #metamodelling #named: C3: A Metamodel for Architecture Description Language based on First-order Connector Types (AA, MO), pp. 76–81.
SAC-2009-LeinoM #reasoning #smt: Reasoning about comprehensions with first-order SMT solvers (KRML, RM), pp. 615–622.
SAC-2009-ZhangLZZZZ #linear #optimisation: Optimizing techniques for saturated arithmetic with first-order linear recurrence (WZ, LL, CZ, HZ, BZ, CZ), pp. 1883–1889.
HPCA-2009-ChenA #fine-grained #parallel #thread #throughput: A first-order fine-grained multithreaded throughput model (XEC, TMA), pp. 329–340.
WRLA-2008-HolenJW09 #calculus #maude #proving: Proof Search for the First-Order Connection Calculus in Maude (BH, EBJ, AW), pp. 173–188.
CSL-2009-AdlerW: Tree-Width for First Order Formulae (IA, MW), pp. 71–85.
CSL-2009-Tatsuta #calculus #commutative: Non-Commutative First-Order Sequent Calculus (MT), pp. 470–484.
LICS-2009-KieronskiT #equivalence #finite #logic #on the #satisfiability: On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations (EK, LT), pp. 123–132.
LICS-2009-MadelaineM #complexity #logic #similarity: The Complexity of Positive First-order Logic without Equality (FRM, BM), pp. 429–438.
LICS-2009-Mimram: The Structure of First-Order Causality (SM), pp. 212–221.
DLT-J-2007-DiekertGK08 #finite #logic #overview #word: A Survey on Small Fragments of First-Order Logic over Finite Words (VD, PG, MK), pp. 513–548.
ICALP-B-2008-BojanczykS #logic #quantifier: Tree Languages Defined in First-Order Logic with One Quantifier Alternation (MB, LS), pp. 233–245.
ICML-2008-KuzelkaZ #estimation #performance: Fast estimation of first-order clause coverage through randomization and maximum likelihood (OK, FZ), pp. 504–511.
KR-2008-BelardinelliL #logic: A Complete First-Order Logic of Knowledge and Time (FB, AL), pp. 705–714.
KR-2008-VassosLL: First-Order Strong Progression for Local-Effect Basic Action Theories (SV, GL, HJL), pp. 662–672.
KR-2008-WittocxMD #approximate #logic #reasoning: Approximate Reasoning in First-Order Logic Theories (JW, MM, MD), pp. 103–112.
SAC-2008-Djelloul #constraints: Combination of decomposability and propagation for solving first-order constraints in decomposable theories (KD), pp. 1728–1732.
CASE-2008-DotoliFM #automation #fault #hybrid #monitoring #petri net: Fault monitoring of automated manufacturing systems by first order hybrid Petri nets (MD, MPF, AMM), pp. 181–186.
SMT-2007-BongioKLLM08 #encoding #proving #smt: Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.
ICLP-2008-NearBF #declarative #logic #named #proving #theorem proving: αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (JPN, WEB, DPF), pp. 238–252.
IJCAR-2008-Korovin #logic #named #proving #theorem proving: iProver — An Instantiation-Based Theorem Prover for First-Order Logic (KK), pp. 292–298.
IJCAR-2008-SchmidtT #logic: A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments (RAS, DT), pp. 194–209.
LICS-2008-Burel #deduction #representation #type system #using: A First-Order Representation of Pure Type Systems Using Superdeduction (GB), pp. 253–263.
ICDAR-2007-EspositoFMB #automation #documentation #incremental #learning #logic #web: Incremental Learning of First Order Logic Theories for the Automatic Annotations of Web Documents (FE, SF, NDM, TMAB), pp. 1093–1097.
DLT-2007-DiekertK #on the #word: On First-Order Fragments for Words and Mazurkiewicz Traces (VD, MK), pp. 1–19.
LATA-2007-Komendantskaya #deduction #network: First-order deduction in neural networks (EK), pp. 307–318.
TLCA-2007-ShkaravskaKE #analysis #polynomial: Polynomial Size Analysis of First-Order Functions (OS, RvK, MCJDvE), pp. 351–365.
SAC-2007-DjelloulDF #constraints #finite #infinity #prolog #theorem proving #towards #unification #using: Toward a first-order extension of Prolog’s unification using CHR: a CHR first-order constraint solver over finite or infinite trees (KD, TBHD, TWF), pp. 58–64.
CADE-2007-DeshaneHJLLM #encoding #proving #satisfiability: Encoding First Order Proofs in SAT (TD, WH, PJ, HL, CL, REM), pp. 476–491.
CSL-2007-Dawar #automaton #locality #logic #model checking: Model-Checking First-Order Logic: Automata and Locality (AD), p. 6.
LICS-2007-AlurABEIL #logic #word: First-Order and Temporal Logics for Nested Words (RA, MA, PB, KE, NI, LL), pp. 151–160.
LICS-2007-CateBV #logic #theorem: Lindstrom theorems for fragments of first-order logic (BtC, JvB, JAV), pp. 280–292.
VMCAI-2007-BouillaguetKWZR #data type #proving #theorem proving #using #verification: Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
KR-2006-ChenLWZ #logic programming #source code: First-Order Loop Formulas for Normal Logic Programs (YC, FL, YW, MZ), pp. 298–307.
KR-2006-SannerM #calculus #hybrid #logic #reasoning: An Ordered Theory Resolution Calculus for Hybrid Reasoning in First-Order Extensions of Description Logic (SS, SAM), pp. 100–111.
KR-2006-ZamanskyA #logic #nondeterminism #semantics: Non-Deterministic Semantics for First-Order Paraconsistent Logics (AZ, AA), pp. 431–439.
SAC-2006-DjelloulD #constraints #finite #formal method #infinity: Solving first-order constraints in the theory of finite or infinite trees: introduction to the decomposable theories (KD, TBHD), pp. 7–14.
FoSSaCS-2006-KuskeL: First-Order and Counting Theories of ω-Automatic Structures (DK, ML), pp. 322–336.
CSL-2006-DurandO #query: First-Order Queries over One Unary Function (AD, FO), pp. 334–348.
ICLP-2006-DaoD #constraints #formal method: Solving First-Order Constraints in the Theory of the Evaluated Trees (TBHD, KD), pp. 423–424.
IJCAR-2006-Rabe #dependent type #logic: First-Order Logic with Dependent Types (FR), pp. 377–391.
LICS-2006-ChaubardPS #composition: First Order Formulas with Modular Predicates (LC, JÉP, HS), pp. 211–220.
LICS-2006-DawarGKS #approximate #optimisation #problem: Approximation Schemes for First-Order Definable Optimisation Problems (AD, MG, SK, NS), pp. 411–420.
LICS-2006-LaroseLT #constraints #problem: A Characterisation of First-Order Constraint Satisfaction Problems (BL, CL, CT), pp. 201–210.
LICS-2006-Otto #bound #logic #monad #problem: The Boundedness Problem for Monadic Universal First-Order Logic (MO), pp. 37–48.
ICML-2005-DriessensD #learning #modelling: Combining model-based and instance-based learning for first order regression (KD, SD), pp. 193–200.
ICML-2005-NatarajanTADFR #learning #modelling #probability: Learning first-order probabilistic models with combining rules (SN, PT, EA, TGD, AF, ACR), pp. 609–616.
FoSSaCS-2005-CalcagnoGH #logic: From Separation Logic to First-Order Logic (CC, PG, MH), pp. 395–409.
CADE-2005-CastelliniS #logic #proving #theorem proving: Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.
CADE-2005-ChaudhuriP #linear #logic #proving #theorem proving: A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.
CADE-2005-ContejeanC #logic #proving #similarity: Reflecting Proofs in First-Order Logic with Equality (EC, PC), pp. 7–22.
CADE-2005-Lev-AmiIRSSY #data type #linked data #logic #open data #reachability #simulation #using #verification: Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures (TLA, NI, TWR, SS, SS, GY), pp. 99–115.
CADE-2005-ZhangSM #decidability: The Decidability of the First-Order Theory of Knuth-Bendix Order (TZ, HBS, ZM), pp. 131–148.
LICS-2005-KieronskiO #decidability #logic: Small Substructures and Decidability Issues for First-Order Logic with Two Variables (EK, MO), pp. 448–457.
PODS-2004-BenediktLBW: A Characterization of First-Order Topological Properties of Planar Spatial Data (MB, CL, JVdB, TW), pp. 107–114.
PODS-2004-Marx #xpath: Conditional XPath, the First Order Complete XPath Dialect (MM), pp. 13–22.
PODS-2004-NashL #data access #query: Processing First-Order Queries under Limited Access Patterns (AN, BL), pp. 307–318.
ICFP-2004-GauthierP #canonical #higher-order #matter #recursion: Numbering matters: first-order canonical forms for second-order recursive types (NG, FP), pp. 150–161.
ICGT-2004-Rensink #graph #logic #representation #using: Representing First-Order Logic Using Graphs (AR), pp. 319–335.
ICML-2004-NatteeSNO #learning #mining #multi: Learning first-order rules from data with multiple parts: applications on mining chemical compound data (CN, SS, MN, TO).
KR-2004-Davis #communication: A First-Order Theory of Communicating First-Order Formulas (ED), pp. 235–245.
DAC-2004-VisweswariahRKWN #analysis #incremental #statistics: First-order incremental block-based statistical timing analysis (CV, KR, KK, SGW, SN), pp. 331–336.
DATE-v1-2004-LegerR: A Digital Test for First-Order [Sigma-Delta] Modulators (GL, AR), pp. 708–709.
TACAS-2004-BeauquierCP #automation #logic #parametricity #protocol #state machine #verification: Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic (DB, TC, EP), pp. 372–387.
CAV-2004-RayH #deduction #pipes and filters #quantifier #using #verification: Deductive Verification of Pipelined Machines Using First-Order Quantification (SR, WAHJ), pp. 31–43.
LICS-2004-DalmauKL #graph #problem #reflexive: First-Order Definable Retraction Problems for Posets and Reflexive Graph (VD, AAK, BL), pp. 232–241.
LICS-2004-GroheS #linear #logic: The Succinctness of First-Order Logic on Linear Orders (MG, NS), pp. 438–447.
RTA-2003-Comon-LundhC #decidability #encryption #logic #protocol: New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols (HCL, VC), pp. 148–164.
POPL-2003-HofmannJ #functional #predict #source code: Static prediction of heap space usage for first-order functional programs (MH, SJ), pp. 185–197.
CADE-2003-Nivelle #axiom #proving: Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms (HdN), pp. 365–379.
CADE-2003-SchmidtH #axiom: A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae (RAS, UH), pp. 412–426.
CSL-2003-Vermeulen #logic #semantics: More Computation Power for a Denotational Semantics for First Order Logic (KFMV), pp. 530–543.
ICLP-2003-Smaus #equation #question #semantics: Is There an Optimal Generic Semantics for First-Order Equations? (JGS), pp. 438–450.
ICALP-2002-Colcombet #decidability #graph #on the #product line #reachability: On Families of Graphs Having a Decidable First Order Theory with Reachability (TC), pp. 98–109.
KR-2002-Lakemeyer #knowledge base #reasoning: Evaluation-Based Reasoning with Disjunctive Information in First-Order Knowledge Bases (GL), pp. 73–81.
SPLC-2002-Mannion #logic #product line #using #validation: Using First-Order Logic for Product Line Model Validation (MM), pp. 176–187.
POPL-2002-SuANPT #constraints #type system: The first-order theory of subtyping constraints (ZS, AA, JN, TP, RT), pp. 203–216.
SAS-2002-ManevichRFGS #representation #static analysis: Compactly Representing First-Order Structures for Static Analysis (RM, GR, JF, DG, SS), pp. 196–212.
FoSSaCS-2002-DanvyN #continuation: A First-Order One-Pass CPS Transformation (OD, LRN), pp. 98–113.
CADE-2002-Hurd #interface #logic: An LCF-Style Interface between HOL and First-Order Logic (JH), pp. 134–138.
CAV-2002-BarrettDS #incremental #satisfiability: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
LICS-2002-FrickG #complexity #higher-order #logic #monad #revisited: The Complexity of First-Order and Monadic Second-Order Logic Revisited (MF, MG), pp. 215–224.
LICS-2002-HodkinsonWZ #branch #decidability #logic: Decidable and Undecidable Fragments of First-Order Branching Temporal Logics (IMH, FW, MZ), pp. 393–402.
ICDAR-2001-BagdanovW #classification #documentation #fine-grained #graph #random #using: Fine-Grained Document Genre Classification Using First Order Random Graphs (ADB, MW), pp. 79–85.
RTA-2001-BonelliKR #higher-order: From Higher-Order to First-Order Rewriting (EB, DK, AR), pp. 47–62.
RTA-2001-VestergaardB #confluence #proving #using #λ-calculus: A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (RV, JB), pp. 306–321.
TLCA-2001-Altenkirch #algebra: Representations of First Order Function Types as Terminal Coalgebras (TA), pp. 8–21.
FLOPS-2001-BozzanoDM #bottom-up #effectiveness #linear #logic programming #semantics #source code: An Effective Bottom-Up Semantics for First-Order Linear Logic Programs (MB, GD, MM), pp. 138–152.
ICEIS-v2-2001-HikitaM #logic #modelling #ontology #process: Business Process Modeling Based on the Ontology and First-Order Logic (TH, MJM), pp. 717–723.
MLDM-2001-MalerbaELL #induction #recognition: First-Order Rule Induction for the Recognition of Morphological Patterns in Topographic Maps (DM, FE, AL, FAL), pp. 88–101.
CSL-2001-Koriche #approximate #logic #reasoning: A Logic for Approximate First-Order Reasoning (FK), pp. 262–276.
IJCAR-2001-BeckertS #calculus #logic: A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities (BB, SS), pp. 626–641.
IJCAR-2001-HodasT #agile #implementation #linear #logic #named #proving #theorem proving: lolliCop — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic (JSH, NT), pp. 670–684.
LICS-2001-Avigad #logic: Eliminating Definitions and Skolem Functions in First-Order Logic (JA), pp. 139–146.
ICALP-2000-LugiezS #decidability #logic: Decidable First-Order Transition Logics for PA-Processes (DL, PS), pp. 342–353.
KR-2000-Massacci #reduction: Reduction rules and universal variables for first order tableaux and DPLL (FM), pp. 186–197.
KR-2000-MontanariPS #automation #deduction #logic: Supporting automated deduction in first-order modal logics (AM, AP, MS), pp. 547–556.
FSE-2000-Jackson #automation #logic #relational: Automating first-order relational logic (DJ), pp. 130–139.
FoSSaCS-2000-Schubert #logic #type inference: Type Inference for First-Order Logic (AS), pp. 297–313.
CADE-2000-Baumgartner #named: FDPLL — A First Order Davis-Putnam-Longeman-Loveland Procedure (PB), pp. 200–219.
CAV-2000-Cohen #encryption #named #protocol #verification: TAPS: A First-Order Verifier for Cryptographic Protocols (EC), pp. 568–571.
CL-2000-Apt #logic #semantics: A Denotational Semantics for First-Order Logic (KRA), pp. 53–69.
LICS-2000-GroheS #on the #query: On First-Order Topological Queries (MG, LS), pp. 349–360.
LICS-2000-Kripke #algorithm #theorem: From the Church-Turing Thesis to the First-Order Algorithm Theorem (SK), p. 177.
LICS-2000-LindellW #decidability #finite: The Role of Decidability in First Order Separations over Classes of Finite Structures (SL, SW), pp. 45–50.
ICALP-1999-FrickG #graph: Deciding First-Order Properties of Locally Tree-Decomposalbe Graphs (MF, MG), pp. 331–340.
FM-v1-1999-Pavlovic #parametricity #semantics #specification: Semantics of First Order Parametric Specifications (DP), pp. 155–172.
FM-v2-1999-Martin #logic: Relating Z and First-Order Logic (AM), pp. 1266–1280.
RTA-1999-DowekHK #higher-order #logic #named: HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic (GD, TH, CK), pp. 317–331.
ASE-1999-FuchsST #logic #natural language: Controlled Natural Language Can Replace First-Order Logic (NEF, US, ST), pp. 295–298.
CADE-1999-DemriG #logic: Tractable Transformations from Modal Provability Logics into First-Order Logic (SD, RG), pp. 16–30.
CADE-1999-KonradW #generative #logic: System Description: Kimba, A Model Generator for Many-Valued First-Order Logics (KK, DAW), pp. 282–286.
CADE-1999-Weidenbach #analysis #automation #logic #protocol #security #towards: Towards an Automatic Analysis of Security Protocols in First-Order Logic (CW), pp. 314–328.
LICS-1999-AtseriasK #finite #fixpoint #logic #set: First-Order Logic vs. Fixed-Point Logic in Finite Set Theory (AA, PGK), pp. 275–284.
PODS-1998-Etessami #morphism: Dynamic Tree Isomorphism via First-Order Updates (KE), pp. 235–243.
ICALP-1998-BorchertKS #on the: On Existentially First-Order Definable Languages and Their Relation to NP (BB, DK, FS), pp. 17–28.
ICML-1998-ReddyT #learning #source code: Learning First-Order Acyclic Horn Programs from Entailment (CR, PT), pp. 472–480.
KR-1998-Levesque #knowledge base #reasoning: A Completeness Result for Reasoning with Incomplete First-Order Knowledge Bases (HJL), pp. 14–23.
ECOOP-1998-BonoF #calculus #imperative: An Imperative, First-Order Calculus with Object Extension (VB, KF), pp. 462–497.
SAS-1998-Volpe #alias #logic programming #source code: A First-Order Language for Expressing Aliasing and Type Properties of Logic Programs (PV), pp. 184–199.
CADE-1998-Pagano #calculus #higher-order #reduction: X.R.S : Explicit Reduction Systems — A First-Order Calculus for Higher-Order Calculi (BP), pp. 72–87.
CAV-1998-XuCSCM #graph #logic #model checking #multi #using: Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (YX, EC, XS, FC, OAM), pp. 219–231.
CSL-1998-KempeS #algebra #on the #power of #specification: On the Power of Quantifers in First-Order Algebraic Specification (DK, AS), pp. 45–57.
CSL-1998-Lukasiewicz #logic #probability #semantics: Many-Valued First-Order Logics with Probabilistic Semantics (TL), pp. 415–429.
LICS-1998-KolaitisO #bound #logic #on the #problem: On the Boundedness Problem for Two-Variable First-Order Logic (PGK, MO), pp. 513–524.
LICS-1998-MullerNT #constraints: The First-Order Theory of Ordering Constraints over Feature Trees (MM, JN, RT), pp. 432–443.
LICS-1998-Viswanathan #abstraction #recursion #type system: Full Abstraction for First-Order Objects with Recursive Types and Subtyping (RV), pp. 380–391.
DLT-1997-Stefaneas #logic: Chartering first order logic (PSS), pp. 579–592.
ICALP-1997-Wilke #logic #strict: Star-Free Picture Expressions are Strictly Weaker Than First-Order Logic (TW), pp. 347–357.
RTA-1997-Marcinkowski: Undecidability of the First Order Theory of One-Step Right Ground Rewriting (JM), pp. 241–253.
RTA-1997-Vorobyov #decidability #linear: The First-Order Theory of One Step Rewriting in Linear Noetherian Systems is Undecidable (SGV), pp. 254–268.
ICML-1997-BottaGP #learning #logic #named: FONN: Combining First Order Logic with Connectionist Learning (MB, AG, RP), pp. 46–56.
ECOOP-1997-Liquori: An Extended Theory of Primitive Objects: FIrst Order System (LL), pp. 146–169.
SAC-1997-ShumskyWME #constraints #finite #generative #heuristic: Direct finite first-order model generation with negative constraint propagation heuristic (OS, RWW, WM, FE), pp. 25–29.
CADE-1997-BjornerSU #integration #reasoning: A Practical Integration of First-Order Reasoning and Decision Procedures (NB, MES, TEU), pp. 101–115.
LICS-1997-EtessamiVW #logic: First-Order Logic with Two Variables and Unary Temporal Logic (KE, MYV, TW), pp. 228–235.
PODS-1996-AbiteboulHB #database #logic #query: Temporal Versus First-Order Logic to Query Temporal Databases (SA, LH, JVdB), pp. 49–57.
ICALP-1996-Pin #automaton #calculus #power of: The Expressive Power of Existential First Order Sentences of Büchi’s Sequential Calculus (JÉP), pp. 300–311.
RTA-1996-Treinen #decidability: The First-Order Theory of One-Step Rewriting is Undecidable (RT), pp. 276–286.
KR-1996-Brafman #statistics: “Statistical” First Order Conditionals (RIB), pp. 398–409.
ALP-1996-Marchiori96a #abstract domain #logic #using: Prime Factorizations of Abstract Domains Using First Order Logic (EM), pp. 209–223.
POPL-1996-GordonR #calculus #similarity #type system: Bisimilarity for a First-Order Calculus of Objects with Subtyping (ADG, GDR), pp. 386–395.
DLT-1995-SchieringT #automaton #logic: Counter-Free Automata, First-Order Logic and Star-Free Expressions (IS, WT), pp. 166–175.
KDD-1995-AugierVK #algorithm #learning #logic #search-based: Learning First Order Logic Rules with a Genetic Algorithm (SA, GV, YK), pp. 21–26.
TAPSOFT-1995-Potthoff #finite #logic: First-Order Logic on Finite Trees (AP), pp. 125–139.
LICS-1995-Dutertre #logic #proving: Complete Proof Systems for First Order Interval Temporal Logic (BD), pp. 36–43.
LICS-1995-ParedaensBG #finite #query: First-order Queries on Finite Structures over the Reals (JP, JVdB, DVG), pp. 79–87.
ICALP-1994-CosmoK #algebra #recursion #term rewriting #λ-calculus: Combining First Order Algebraic Rewriting Systems, Recursion and Extensional λ Calculi (RDC, DK), pp. 462–472.
KR-1994-Koubarakis #complexity #constraints: Complexity Results for First-Order Theories of Temporal Constraints (MK), pp. 379–390.
KR-1994-LakemeyerM #decidability #power of: Enhancing the Power of a Decidable First-Order Reasoner (GL, SM), pp. 403–414.
SEKE-1994-Sakalauskaite #branch #calculus #logic: A complete sequent calculus for a first order branching temporal logic (JS), pp. 274–280.
ALP-1994-BidoitH #behaviour #logic #proving #standard #theorem: Proving Behavioural Theorems with Standard First-Order Logic (MB, RH), pp. 41–58.
LOPSTR-1994-TarauD #continuation #logic programming: Logic Programming and Logic Grammars with First-Order Continuations (PT, VD), pp. 215–230.
CADE-1994-ChuP #proving #semantics #theorem proving #using: Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.
CADE-1994-SturgillS #logic #novel #parallel: A Novel Asynchronous Parallelism Scheme for First-Order Logic (DBS, AMS), pp. 484–498.
ILPS-1994-McCartyS #interpreter #logic #prolog: A PROLOG Interpreter for First-Order Intuitionistic Logic (LTM, LAS), p. 685.
LICS-1994-LincolnS #calculus #linear #logic #proving: Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi (PL, NS), pp. 282–291.
LICS-1994-Sewell #axiom #bisimulation #equation: Bisimulation is Not Finitely (First Order) Equationally Axiomatisable (PS), pp. 62–70.
RTA-1993-NivelaN: Saturation of First-Order (Constrained) Clauses with the Saturate System (PN, RN), pp. 436–440.
ICALP-1992-Straubing #complexity #power of: Circuit Complexity and the Expressive Power of Generalized First-Order Formulas (HS), pp. 16–27.
SEKE-1992-Reif #correctness #specification: Correctness of Full First-Order Specifications (WR), pp. 276–283.
ALP-1992-AptMP #formal method #prolog: A Theory of First-Order Built-in’s of Prolog (KRA, EM, CP), pp. 69–83.
ALP-1992-BachmairGW #proving #theorem proving: Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
WSA-1992-Hamilton #analysis #functional #lazy evaluation #source code: Sharing Analysis of Lazy First-Order Functional Programs (GWH), pp. 68–78.
STOC-1992-GroveHK #logic: Asymptotic Conditional Probabilities for First-Order Logic (AJG, JYH, DK), pp. 294–305.
CADE-1992-Fisher #normalisation: A Normal Form for First-Order Temporal Formulae (MF), pp. 370–384.
RTA-1991-Deruyver #equation #logic #named #proving #theorem proving: EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.
ML-1991-RichardsM: First-Order Theory Revision (BLR, RJM), pp. 447–451.
POPL-1991-JoungS #coordination #interactive #multi: Coordinating First-Order Multiparty Interactions (YJJ, SAS), pp. 209–220.
WSA-1991-Chin #deforestation #functional #source code: Generalising Deforestation for All First-Order Functional Programs (WNC), pp. 173–181.
CSL-1991-Dahlhaus #how #memory management #modelling: How to Implement First Order Formulas in Local Memory Machine Models (ED), pp. 68–78.
CSL-1991-Oguztuzun #equivalence #logic: A Fragment of First Order Logic Adequate for Observation Equivalence (HO), pp. 278–292.
ICLP-1991-Sato #logic programming: Full First Order Logic Programming and Truth Predicate (TS), p. 948.
ISLP-1991-Carpenter: Typed Feature Structures: A Generalization of First-Order Terms (BC), pp. 187–201.
ISLP-1991-SatoM #interpreter #source code #top-down: A Complete Top-Down Interpreter for First Order Programs (TS, FM), pp. 35–53.
LICS-1991-AvronH #database #on the #query: On First Order Database Query Languages (AA, YH), pp. 226–231.
LICS-1991-KiferW #logic programming #morphism #polymorphism: A First-Order Theory of Types and Polymorphism in Logic Programming (MK, JW), pp. 310–321.
ALP-1990-Sato #equivalence: An Equivalence Preserving First Order Unfold/fold Transformation System (TS), pp. 173–188.
CADE-1990-PymW: Investigations into Proof-Search in a System of First-Order Dependent Function Types (DJP, LAW), pp. 236–250.
CLP-1990-LauP90 #logic #recursion #specification #synthesis #top-down: Top-down Synthesis of Recursive Logic Procedures from First-order Logic Specifications (KKL, SDP), pp. 667–684.
PODS-1989-Cosmadakis #on the #query #recursion: On the First-Order Expressibility of Recursive Queries (SSC), pp. 311–323.
FPCA-1989-BjernerH #analysis #approach #composition #functional #lazy evaluation #source code: A Composition Approach to Time Analysis of First Order Lazy Functional Programs (BB, SH), pp. 157–165.
KR-1989-McAllesterGF #syntax #taxonomy: Taxonomic Syntax for First Order Inference (DAM, RG, TF), pp. 289–300.
CSL-1989-Ohlbach #logic #multi #proving: New Ways for Developing Proof Theories for First-Order Multi Modal Logics (HJO), pp. 271–308.
LICS-1989-AbiteboulV #fixpoint #logic: Fixpoint Extensions of First-Order Logic and Datalog-Like Languages (SA, VV), pp. 71–79.
NACLP-1989-ChenKW #higher-order #logic programming #named #semantics: HiLog: A First-Order Semantics for Higher-Order Logic Programming Constructs (WC, MK, DSW), pp. 1090–1114.
ML-1988-Helft #learning: Learning Systems of First-Order Rules (NH), pp. 395–401.
ML-1988-MuggletonB: Machine Invention of First Order Predicates by Inverting Resolution (SM, WLB), pp. 339–352.
CADE-1988-ZhangK #proving #theorem proving #using: First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.
LICS-1987-BachmairD #proving #theorem proving: Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
LICS-1987-Emden #functional #logic #programming #relational: First-order Predicate Logic as a Common Basis for Relational and Functional Programming (MHvE), p. 179.
LICS-1987-Thomas #infinity #logic #on the: On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees (WT), pp. 245–256.
PODS-1986-Naqvi #query: Negation as Failure for First-Order Queries (SAN), pp. 114–122.
CADE-1986-BuningL #satisfiability: Classes of First Order Formulas Under Various Satisfiability Definitions (HKB, TL), pp. 553–563.
LICS-1986-Mason #equivalence #lisp #proving #source code: Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation (IAM), pp. 105–117.
SLP-1985-UmrigarP85 #empirical #logic #programming: An Experiment in Programming with Full First-Order Logic (ZDU, VP), pp. 40–47.
SLP-1984-AponteFR84 #editing #proving: Editing First-Order Proofs: Programmed Rules vs Derived Rules (MVA, JAF, PR), pp. 92–98.
CADE-1982-HenschenN #database #infinity #recursion #representation #sequence: Representing Infinite Sequences of Resolvents in recursive First-Order Horn Databases (LJH, SAN), pp. 342–359.
STOC-1980-Yap #problem #source code #trade-off: Space-time Tradeoffs and First Order Problems in a Model of Programs (CKY), pp. 318–325.
POPL-1979-CartwrightM #logic #programming: First Order Programming Logic (RC, JM), pp. 68–80.
SIGMOD-1978-Nicolas #dependence #formal method #functional #logic #multi: First Order Logic Formalization for Functional, Multivalued and Mutual Dependencies (JMN), pp. 40–46.
STOC-1972-JonesS #similarity #turing machine: Turing Machines and the Spectra of First-Order Formulas with Equality (NDJ, ALS), pp. 157–167.