Found 100 Documents (Results 1–100)
A uniform formalisation of three-valued logics in bisequent calculus. (English) Zbl 07838495
Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 325-343 (2023).
Choose your colour: tree interpolation for quantified formulas in SMT. (English) Zbl 07838491
Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 248-265 (2023).
Uniform interpolants in \(\mathcal{EUF}\): algorithms using DAG-representations. (English) Zbl 07566058
Semiconic Idempotent Logic II: Beth Definability and Deductive Interpolation. arXiv:2208.09724
Preprint, arXiv:2208.09724 [math.LO] (2022).
Interpolation in 16-valued trilattice logics. (English) Zbl 1437.03100
Reviewer: Albert Hoogewijs (Gent)
Representation theorems and locality for subsumption testing and interpolation in the description logics \(\mathcal{EL}\), \(\mathcal{EL}^+\) and their extensions with \(n\)-ary roles and numerical domains. (English) Zbl 1393.68161
Reviewer: Éric Martin (Sydney)
The Boolean solution problem from the perspective of predicate logic. (English) Zbl 1496.03262
Dixon, Clare (ed.) et al., Frontiers of combining systems. 11th international symposium, FroCoS 2017, Brasília, Brazil, September 27–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10483, 333-350 (2017).
On perception-based logical deduction with fuzzy inputs. (English) Zbl 1455.68209
Carvalho, Joao Paulo (ed.) et al., Information processing and management of uncertainty in knowledge-based systems. 16th international conference, IPMU 2016, Eindhoven, The Netherlands, June 20–24, 2016. Proceedings. Part II. Cham: Springer. Commun. Comput. Inf. Sci. 611, 495-509 (2016).
Definability in first order theories of graph orderings. (English) Zbl 1476.03040
Artemov, Sergei (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4–7, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9537, 331-348 (2016).
Adjacent and weak adjacent. (Chinese. English summary) Zbl 1374.06012
Machine-checked interpolation theorems for substructural logics using display calculi. (English) Zbl 1476.03007
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 452-468 (2016).
Interpolant synthesis for quadratic polynomial inequalities and combination with EUF. (English) Zbl 1475.03072
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 195-212 (2016).
Labelled interpolation systems for hyper-resolution, clausal, and local proofs. (English) Zbl 1356.68199
Uniform interpolation for coalgebraic fixpoint logic. (English) Zbl 1366.03245
Moss, Lawrence S. (ed.) et al., 6th conference on algebra and coalgebra in computer science, CALCO’15, Nijmegen, Netherlands, June 24–26, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-84-2). LIPIcs – Leibniz International Proceedings in Informatics 35, 238-252 (2015).
Interpolation systems for ground proofs in automated deduction: a survey. (English) Zbl 1356.68179
MSC:
68T15
03B35
Pre-Hilbert spaces with anomalous splitting and orthogonally-closed subspace structures. (English) Zbl 1318.46011
Amalgamation and interpolation in ordered algebras. (English) Zbl 1318.06012
Reviewer: Michiro Kondo (Inzai)
Interpolant strength revisited. (English) Zbl 1273.03051
Cimatti, Alessandro (ed.) et al., Theory and applications of satisfiability testing – SAT 2012. 15th international conference, Trento, Italy, June 17–20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31611-1/pbk). Lecture Notes in Computer Science 7317, 312-326 (2012).
Efficient generation of Craig interpolants in satisfiability modulo theories. (English) Zbl 1351.68247
An interpolating sequent calculus for quantifier-free Presburger arithmetic. (English) Zbl 1291.03112
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 384-399 (2010).
Definability in the subword order. (English) Zbl 1286.03132
Ferreira, Fernando (ed.) et al., Programs, proofs, processes. 6th conference on computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30–July 4, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13961-1/pbk). Lecture Notes in Computer Science 6158, 246-255 (2010).
Propositional interpolation and abstract interpretation. (English) Zbl 1259.03024
Gordon, Andrew D. (ed.), Programming languages and systems. 19th European symposium on programming, ESOP 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11956-9/pbk). Lecture Notes in Computer Science 6012, 185-204 (2010).
Interpolant strength. (English) Zbl 1273.68225
Barthe, Gilles (ed.) et al., Verification, model checking, and abstract interpretation. 11th international conference, VMCAI 2010, Madrid, Spain, January 17–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11318-5/pbk). Lecture Notes in Computer Science 5944, 129-145 (2010).
On several proofs of the recognizability theorem. (English) Zbl 1256.03042
Bozapalidis, Symeon (ed.) et al., Algebraic informatics. Third international conference, CAI 2009, Thessaloniki, Greece, May 19–22, 2009, Proceedings. Berlin: Springer (ISBN 978-3-642-03563-0/pbk). Lecture Notes in Computer Science 5725, 78-80 (2009).
Interpolation and symbol elimination. (English) Zbl 1250.68193
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 199-213 (2009).
Ground interpolation for combined theories. (English) Zbl 1250.68188
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 183-198 (2009).
Interpolant generation for UTVPI. (English) Zbl 1250.68186
Schmidt, Renate A. (ed.), Automated deduction – CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2–7, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02958-5/pbk). Lecture Notes in Computer Science 5663. Lecture Notes in Artificial Intelligence, 167-182 (2009).
Rewriting interpolants. (English) Zbl 1286.03039
Chen, Yixiang (ed.) et al., Proceedings of the 1st international conference on foundations of informatics, computing and software (FICS 2008), East China Normal University, Shanghai, China, June 3–6, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 212, 163-176 (2008).
Elimination problems in logic: a brief history. (English) Zbl 1169.03002
Reviewer: Victor V. Pambuccian (Phoenix)
Interpolation in local theory extensions. (English) Zbl 1170.03018
Reviewer: Nail Zamov (Kazan)
Mechanising a proof of Craig’s interpolation theorem for intuitionistic logic in nominal Isabelle. (English) Zbl 1166.68340
Autexier, Serge (ed.) et al., Intelligent computer mathematics. 9th international conference, AISC 2008, 15th symposium, Calculemus 2008, 7th international conference, MKM 2008, Birmingham, UK, July 28–August 1, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85109-7/pbk). Lecture Notes in Computer Science 5144. Lecture Notes in Artificial Intelligence, 38-52 (2008).
Effect algebras with the subsequential interpolation property. (English) Zbl 1153.81005
Reviewer: Horst Szambien (Garbsen)
On the preservation of the properties of many-sorted algebraic systems. (Russian. English summary) Zbl 1167.03302
Automatic recognition of interpolation in modal calculi. (Russian, English) Zbl 1164.03301
Algebra Logika 46, No. 1, 103-119 (2007); translation in Algebra Logic 46, No. 1, 62-70 (2007).
A combination method for generating interpolants. (English) Zbl 1135.03331
Nieuwenhuis, Robert (ed.), Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28005-7/pbk). Lecture Notes in Computer Science 3632. Lecture Notes in Artificial Intelligence, 353-368 (2005).
Fuzzy logic and \(\omega^{+}\)-valued logic. (Russian. English summary) Zbl 1249.03031
Quantum logics with the Riesz interpolation property. (English) Zbl 1051.03052
Reviewer: Mirko Navara (Praha)
Compressible groups. (English) Zbl 1068.06018
Infinitary lattice and Riesz properties of pseudoeffect algebras and po-groups. (English) Zbl 1044.06008
Reviewer: Jānis Cīrulis (Riga)
Product effect algebras. (English) Zbl 1014.81004
Moment problem and spectral theorem. (English) Zbl 0996.81023
Reviewer: Todor D.Todorov (San Luis Obispo)
Effect algebras which can be covered by MV-algebras. (English) Zbl 1022.06005
Reviewer: D.Mundici (Firenze)
An extended joint consistency theorem for a nonconstructive logic of partial terms with definite descriptions. (English) Zbl 0988.03049
Doing logic by computer: Interpolation in fragments of intuitionistic propositional logic. (English) Zbl 0959.03006
Positive operator measures determined by their moment sequences. (English) Zbl 0952.47054
Reviewer: Chandra Shekhar Sharma (London)
Logical questions concerning the \(\mu\)-calculus: Interpolation, Lyndon and Łoś-Tarski. (English) Zbl 0982.03011
Reviewer: Petr Jančar (Ostrava)
An extension of the Cobham-Semënov theorem. (English) Zbl 0958.03025
Reviewer: R.Villemaire (Montréal)
No feasible monotone interpolation for cut-free Gentzen type propositional calculus with permutation inference. (English) Zbl 0960.03046
Calude, C. S. (ed.) et al., Combinatorics, computation & logic. Proceedings of DMTCS ’99 and CATS ’99. Auckland, New Zealand, January 18-21, 1999. Singapore: Springer. Aust. Comput. Sci. Commun. 21, 3, 106-116 (1999).
The super-amalgamation property of the variety of ortholattices. (English) Zbl 0948.03058
Reviewer: M.Abad (Bahia Blanca)
Lambek calculus and formal grammars. (English) Zbl 0933.03019
Beklemishev, Lev et al., Provability, complexity, grammars. Three doctoral dissertations translated from the Russian. Providence, RI: American Mathematical Society. Transl., Ser. 2, Am. Math. Soc. 192, 57-86 (1999).
Reviewer: Mirosława Kołowska-Gawiejnowicz (Poznań)
Uniform interpolation, automata and the modal \(\mu\)-calculus. (English) Zbl 0906.03018
Kracht, Marcus (ed.) et al., Advances in modal logic. Vol. 1. Selected papers of the 1st AiML conference, Free University of Berlin, Germany, October 1996. Stanford, CA: Center for the Study of Language and Information (CSLI). CSLI Lect. Notes. 87, 73-84 (1998).
Interpolants, cut elimination and flow graphs for the propositional calculus. (English) Zbl 0873.03050
Reviewer: M.Yasuhara (Princeton)
Making proofs without modus ponens: An introduction to the combinatorics and complexity of cut elimination. (English) Zbl 0873.03049
Reviewer: M.Yasuhara (Princeton)
The Craig interpolation theorem for schematic systems. (English) Zbl 0855.03031
Collegium logicum. Annals of the Kurt Gödel Society. Volume 2. Wien: Springer-Verlag. 87-100 (1996).
Reviewer: M.Yasuhara (Princeton)
The relation between inference and interpolation in the framework of fuzzy systems. (English) Zbl 0891.93053
MSC:
93C42
Constructing Craig interpolation formulas. (English) Zbl 1527.03007
Du, Ding-Zhu (ed.) et al., Computing and combinatorics. 1st international conference, COCOON ’95, Xi’an, China, August 24–26, 1995. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 959, 181-190 (1995).
Linguistically oriented fuzzy logic control and its design. (English) Zbl 0871.93032
Reviewer: D.Franke (Hamburg)
A note on definability in equational logic. (English) Zbl 0812.03015
Reviewer: H.-J.Vogel (Potsdam)
A new, simpler proof of the modularisation theorem for logical specifications. (English) Zbl 0798.03032
MSC:
03B70
On an interpretation of second order quantification in first order intuitionistic propositional logic. (English) Zbl 0763.03009
Semi-analytic tableaux for propositional normal modal logics with application to nonmonotonicity. (English) Zbl 0799.03015
Experiments with 1-D and 2-D signals using Gibbs derivatives. (English) Zbl 0728.42017
Gibbs derivatives, Proc. 1st Int. Workshop, Kupari-Dubrovnik/Yugosl. 1989, 181-196 (1990).
Reviewer: D.S.Lubinsky (Wits)
A compact representation of proofs. (English) Zbl 0644.03033
Reviewer: P.Štěpánek
Monadic second order definable relations on the binary tree. (English) Zbl 0628.03005
Reviewer: N.Both
On enumerability of interpolants. (English) Zbl 0536.03002
Algebraic Conf., Novi Sad/Yugosl. 1981, 71-78 (1982).
Reviewer: A.Kreczmar
The logical study of science. (English) Zbl 0486.03007
Semantical investigations in Heyting’s intuitionistic logic. (English) Zbl 0453.03001
Synthese Library, Vol. 148. Dordrecht - Boston - London: D. Reidel Publishing Company. X, 287 p. Dfl. 100.00; $ 52.50 (1981).
Two remarks on Boolean algebras. (English) Zbl 0493.03037
Algebraic conference, Skopje 1980, 35-41 (1980).
Structural and algorithmic peculiarities of the arithmetic-logical construction of a processor for the additive Fourier transform. (Russian) Zbl 0439.65114
Mat. Model. Teor. Ehlektr. Tsepej 16, 66-72 (1978).
The use of a fast multidimensional Fourier transformation for polynomial representation of multiple-valued logic functions. (English. Russian original) Zbl 0436.65109
Eng. Cybern. 16, No. 5, 152-155 (1978); translation from Izv. Akad. Nauk SSSR, Tekh. Kibern. 1978, No. 5, 202-205 (1978).
Logical synthesis by means of Fourier-transformations of Boolean functions. (Russian) Zbl 0421.94025
Filter Results by …
Document Type
- Journal Articles (70)
- Collection Articles (28)
- Books (1)
- arXiv Preprints (1)
all
top 5
Author
- Dvurečenskij, Anatolij (7)
- Weissenbacher, Georg (3)
- Bonacina, Maria Paola (2)
- Cimatti, Alessandro (2)
- D’Agostino, Giovanna (2)
- D’silva, Vijay (2)
- Foulis, David James (2)
- Fussner, Wesley (2)
- Galatos, Nikolaos (2)
- Goel, Amit (2)
- Goré, Rajeev Prabhakar (2)
- Griggio, Alberto (2)
- Hoenicke, Jochen (2)
- Hollenberg, Marco (2)
- Johansson, Moa (2)
- Kapur, Deepak (2)
- Kröning, Daniel (2)
- Krstic, Sava A. (2)
- Madarász, Judit X. (2)
- Maksimova, Larisa L’vovna (2)
- Metcalfe, George (2)
- Novák, Vilém (2)
- Pitts, Andrew M. (2)
- Sebastiani, Roberto (2)
- Sofronie-Stokkermans, Viorica (2)
- Thinniyam, Ramanathan S. (2)
- Tinelli, Cesare (2)
- Wernhard, Christoph (2)
- Arai, Noriko H. (1)
- Avallone, Anna (1)
- Benedikt, Michael A. (1)
- Bès, Alexis (1)
- Beyersdorff, Olaf (1)
- Bloom, Stephen L. (1)
- Bonet, Maria Luisa (1)
- Borzyszkowski, Tomasz (1)
- Bourhis, Pierre (1)
- Brillout, Angelo (1)
- Brotherston, James (1)
- Buhagiar, David (1)
- Carbone, Alessandra (1)
- Chapman, Peter (1)
- Chen, Mingshuai (1)
- Chetcuti, Emmanuel (1)
- Chew, Leroy (1)
- Christ, Jürgen (1)
- Courcelle, Bruno (1)
- Dai, Liyun (1)
- Dawson, Jeremy E. (1)
- Domingo, Carlos (1)
- Duchoň, Miloslav (1)
- Dvořák, Antonín (1)
- Ecsedi-Toth, Peter (1)
- Foley, Thomas A. (1)
- Fuchs, Alexander (1)
- Gabbay, Dov M. (1)
- Gan, Ting (1)
- Gavaldà, Ricard (1)
- Georgescu, George (1)
- Ghilardi, Silvio (1)
- Gianola, Alessandro (1)
- Grundy, Jim (1)
- Gumb, Raymond D. (1)
- Hendriks, Lex (1)
- Henkel, Elisabeth (1)
- Huang, Guoxiang (1)
- Indrzejczak, Andrzej (1)
- Katkov, A. F. (1)
- Klawonn, Frank (1)
- Kovács, Laura Ildikó (1)
- Kowalski, Tomasz (1)
- Kudinov, Oleg Victorovich (1)
- Labunets, V. G. (1)
- Lahti, Pekka Johannes (1)
- Läuchli, Hans (1)
- Lefever, Koen (1)
- Lu, Tao (1)
- Lynch, Christopher A. (1)
- Maciel, Alexis (1)
- Mahajan, Meena (1)
- Markova, Valentina P. (1)
- Marti, Johannes (1)
- McKinna, James (1)
- McMillan, Kenneth L. (1)
- Mijajlović, Žarko (1)
- Miller, Dale Allen (1)
- Miyazaki, Yutaka (1)
- Montagna, Franco (1)
- Mundici, Daniele (1)
- Muskens, Reinhard A. (1)
- Musuvathi, Madanlal (1)
- Nagul, Nadezhda Vladimirovna (1)
- Pentus, Mati (1)
- Petrukhin, Yaroslav Igorevich (1)
- Pichler, Franz Rupert (1)
- Pitassi, Toniann (1)
- Ponomaryov, Denis K. (1)
- Pták, Pavel (1)
- Pulmannová, Sylvia (1)
- Purandare, Mitra (1)
- and 40 more Authors
all
top 5
Serial
- Stud. Log. (6)
- J. Autom. Reasoning (5)
- Log. Methods Comput. Sci. (5)
- Int. J. Theor. Phys. (4)
- J. Symb. Log. (4)
- Ann. Pure Appl. Logic (4)
- Algebra Logika (2)
- Math. Nachr. (2)
- Math. Slovaca (2)
- Rep. Math. Logic (2)
- Synthese (2)
- Theor. Comput. Sci. (2)
- J. Comput. Phys. (1)
- Lett. Math. Phys. (1)
- Rep. Math. Phys. (1)
- Algebra Logic (1)
- Fuzzy Sets Syst. (1)
- J. Algebra (1)
- J. Philos. Log. (1)
- J. Pure Appl. Algebra (1)
- Log. Anal., Nouv. Sér. (1)
- Eng. Cybern. (1)
- Hist. Philos. Log. (1)
- J. Inf. Process. Cybern. (1)
- Int. J. Approx. Reasoning (1)
- J. Log. Comput. (1)
- Atti Accad. Naz. Lincei, VIII. Ser., Rend., Cl. Sci. Fis. Mat. Nat. (1)
- Bull. Am. Math. Soc., New Ser. (1)
- Comput. Complexity (1)
- Vychisl. Sist. (1)
- J. Appl. Non-Class. Log. (1)
- Bull. IGPL (1)
- Soft Comput. (1)
- Fundam. Inform. (1)
- Jt. Bull. NCC IIS, Ser. Comput. Sci. (1)
- J. Tianjin Norm. Univ., Nat. Sci. Ed. (1)
- J. Aust. Math. Soc. (1)
- Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform. (1)
- Vestn. Samar. Gos. Univ., Estestvennonauchn. Ser. (1)
- ACM Trans. Comput. Log. (1)
- Found. Phys. (1)
- Synth. Libr. (1)
all
top 5
Year of Publication
- 2024 (1)
- 2023 (2)
- 2022 (2)
- 2021 (2)
- 2020 (1)
- 2019 (3)
- 2018 (1)
- 2017 (3)
- 2016 (7)
- 2015 (3)
- 2014 (2)
- 2012 (3)
- 2010 (5)
- 2009 (4)
- 2008 (6)
- 2007 (2)
- 2006 (1)
- 2005 (3)
- 2004 (3)
- 2003 (2)
- 2002 (4)
- 2001 (3)
- 2000 (4)
- 1999 (4)
- 1998 (2)
- 1997 (2)
- 1996 (2)
- 1995 (2)
- 1994 (1)
- 1993 (2)
- 1992 (1)
- 1991 (1)
- 1990 (1)
- 1989 (1)
- 1987 (2)
- 1983 (1)
- 1982 (3)
- 1981 (1)
- 1980 (2)
- 1978 (4)
- 1977 (1)
all
top 3
Software
- FOCI (13)
- CSIsat (4)
- Princess (4)
- SIMPLIFY (4)
- z3 (3)
- BLAST (2)
- Chaff (2)
- Easychair (2)
- MiniSat (2)
- SMTInterpol (2)
- VAMPIRE (2)
- Wolverine (2)
- ABC (1)
- Automath (1)
- CVC Lite (1)
- CoFI (1)
- DPT (1)
- Datalog LITE (1)
- E Theorem Prover (1)
- E-KRHyper (1)
- E-SETHEO (1)
- ESC/Java (1)
- FEMaLeCoP (1)
- ICS (1)
- Isabelle (1)
- Isabelle/HOL (1)
- Mace4 (1)
- MathSAT (1)
- MathSAT5 (1)
- Mcmt (1)
- Nominal Isabelle (1)
- PTTP (1)
- PeRIPLO (1)
- PicoSAT (1)
- Prover9 (1)
- Quaffle (1)
- SATCHMO (1)
- SDPT3 (1)
- SETHEO (1)
- SLAB (1)
- SMT-LIB (1)
- SPASS (1)
- VeriFun (1)
- Zapato (1)
- leanCoP (1)
